Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clcnvlem Structured version   Visualization version   Unicode version

Theorem clcnvlem 36230
 Description: When , an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
Hypotheses
Ref Expression
clcnvlem.sub1
clcnvlem.sub2
clcnvlem.sub3
clcnvlem.ssub
clcnvlem.ubex
clcnvlem.clex
Assertion
Ref Expression
clcnvlem
Distinct variable groups:   ,   ,,   ,,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem clcnvlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 clcnvlem.ubex . . . 4
2 clcnvlem.ssub . . . . 5
3 clcnvlem.clex . . . . 5
42, 3jca 535 . . . 4
5 clcnvlem.sub3 . . . . 5
65cleq2lem 36214 . . . 4
71, 4, 6elabd 36178 . . 3
87cnvintabd 36209 . 2
9 df-rab 2746 . . . . 5
10 exsimpl 1729 . . . . . . . . . . 11
11 relcnv 5207 . . . . . . . . . . . . 13
12 releq 4917 . . . . . . . . . . . . 13
1311, 12mpbiri 237 . . . . . . . . . . . 12
1413exlimiv 1776 . . . . . . . . . . 11
1510, 14syl 17 . . . . . . . . . 10
16 df-rel 4841 . . . . . . . . . 10
1715, 16sylib 200 . . . . . . . . 9
18 selpw 3958 . . . . . . . . . 10
1918bicomi 206 . . . . . . . . 9
2017, 19sylib 200 . . . . . . . 8
2120pm4.71ri 639 . . . . . . 7
2221bicomi 206 . . . . . 6
2322abbii 2567 . . . . 5
249, 23eqtri 2473 . . . 4
2524inteqi 4238 . . 3
2625a1i 11 . 2
27 vex 3048 . . . . . . 7
2827cnvex 6740 . . . . . 6
2928cnvex 6740 . . . . 5
3029a1i 11 . . . 4
311, 2ssexd 4550 . . . . . . . . . . 11
32 difexg 4551 . . . . . . . . . . 11
3331, 32syl 17 . . . . . . . . . 10
34 unexg 6592 . . . . . . . . . 10
3528, 33, 34sylancr 669 . . . . . . . . 9
36 inundif 3845 . . . . . . . . . . . . . 14
37 cnvun 5241 . . . . . . . . . . . . . . . . . . . . 21
3837sseq1i 3456 . . . . . . . . . . . . . . . . . . . 20
3938biimpi 198 . . . . . . . . . . . . . . . . . . 19
4039unssad 3611 . . . . . . . . . . . . . . . . . 18
41 relcnv 5207 . . . . . . . . . . . . . . . . . . . . 21
42 relin2 4952 . . . . . . . . . . . . . . . . . . . . 21
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
44 dfrel2 5286 . . . . . . . . . . . . . . . . . . . 20
4543, 44mpbi 212 . . . . . . . . . . . . . . . . . . 19
46 cnvss 5007 . . . . . . . . . . . . . . . . . . 19
4745, 46syl5eqssr 3477 . . . . . . . . . . . . . . . . . 18
4840, 47syl 17 . . . . . . . . . . . . . . . . 17
49 ssid 3451 . . . . . . . . . . . . . . . . 17
50 unss12 3606 . . . . . . . . . . . . . . . . 17
5148, 49, 50sylancl 668 . . . . . . . . . . . . . . . 16
5251a1i 11 . . . . . . . . . . . . . . 15
53 cnveq 5008 . . . . . . . . . . . . . . . 16
5453sseq1d 3459 . . . . . . . . . . . . . . 15
55 sseq1 3453 . . . . . . . . . . . . . . 15
5652, 54, 553imtr3d 271 . . . . . . . . . . . . . 14
5736, 56ax-mp 5 . . . . . . . . . . . . 13
58 sseq2 3454 . . . . . . . . . . . . 13
5957, 58syl5ibr 225 . . . . . . . . . . . 12
6059adantl 468 . . . . . . . . . . 11
61 clcnvlem.sub1 . . . . . . . . . . 11
6260, 61anim12d 566 . . . . . . . . . 10
63 cnveq 5008 . . . . . . . . . . . 12
64 cnvun 5241 . . . . . . . . . . . . 13
65 cnvnonrel 36194 . . . . . . . . . . . . . . 15
66 0ss 3763 . . . . . . . . . . . . . . 15
6765, 66eqsstri 3462 . . . . . . . . . . . . . 14
68 ssequn2 3607 . . . . . . . . . . . . . 14
6967, 68mpbi 212 . . . . . . . . . . . . 13
7064, 69eqtr2i 2474 . . . . . . . . . . . 12
7163, 70syl6reqr 2504 . . . . . . . . . . 11
7271adantl 468 . . . . . . . . . 10
7362, 72jctild 546 . . . . . . . . 9
7435, 73spcimedv 3133 . . . . . . . 8
7574imp 431 . . . . . . 7
7675adantlr 721 . . . . . 6
77 eqeq1 2455 . . . . . . . . 9
7877anbi1d 711 . . . . . . . 8
7978exbidv 1768 . . . . . . 7
8079ad2antlr 733 . . . . . 6
8176, 80mpbird 236 . . . . 5
8281ex 436 . . . 4
83 cnvcnvss 5290 . . . . 5
8483a1i 11 . . . 4
8530, 82, 84intabssd 36216 . . 3
86 vex 3048 . . . . 5
8786a1i 11 . . . 4
88 eqtr 2470 . . . . . . . 8
89 cnvss 5007 . . . . . . . . . . . 12
90 sseq2 3454 . . . . . . . . . . . 12
9189, 90syl5ibr 225 . . . . . . . . . . 11
9291adantl 468 . . . . . . . . . 10
93 clcnvlem.sub2 . . . . . . . . . 10
9492, 93anim12d 566 . . . . . . . . 9
9594ex 436 . . . . . . . 8
9688, 95syl5 33 . . . . . . 7
9796impl 626 . . . . . 6
9897expimpd 608 . . . . 5
9998exlimdv 1779 . . . 4
100 ssid 3451 . . . . 5
101100a1i 11 . . . 4
10287, 99, 101intabssd 36216 . . 3
10385, 102eqssd 3449 . 2
1048, 26, 1033eqtrd 2489 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1444  wex 1663   wcel 1887  cab 2437  crab 2741  cvv 3045   cdif 3401   cun 3402   cin 3403   wss 3404  c0 3731  cpw 3951  cint 4234   cxp 4832  ccnv 4833   wrel 4839 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-int 4235  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fv 5590  df-1st 6793  df-2nd 6794 This theorem is referenced by:  cnvtrucl0  36231  cnvrcl0  36232  cnvtrcl0  36233
 Copyright terms: Public domain W3C validator