ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  enwomnilem Unicode version
Theorem enwomnilem 7509
Description: Lemma for enwomni 7510. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
Assertion
Ref Expression
enwomnilem |- ( A ~~ B -> ( A e. WOmni -> B e. WOmni ) )
Proof of Theorem enwomnilem
Dummy variables f g h x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 7030 . . . . . . 7 |- ( A ~~ B <-> E. h h : A -1-1-onto-> B )
21biimpi 120 . . . . . 6 |- ( A ~~ B -> E. h h : A -1-1-onto-> B )
32ad2antrr 492 . . . . 5 |- ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) -> E. h h : A -1-1-onto-> B )
4 fveq1 5694 . . . . . . . . . 10 |- ( f = ( g o. h ) -> ( f ` x ) = ( ( g o. h ) ` x ) )
54eqeq1d 2247 . . . . . . . . 9 |- ( f = ( g o. h ) -> ( ( f ` x ) = 1o <-> ( ( g o. h ) ` x ) = 1o ) )
65ralbidv 2550 . . . . . . . 8 |- ( f = ( g o. h ) -> ( A. x e. A ( f ` x ) = 1o <-> A. x e. A ( ( g o. h ) ` x ) = 1o ) )
76dcbid 850 . . . . . . 7 |- ( f = ( g o. h ) -> (DECID A. x e. A ( f ` x ) = 1o <-> DECID A. x e. A ( ( g o. h ) ` x ) = 1o ) )
8 iswomnimap 7506 . . . . . . . . 9 |- ( A e. WOmni -> ( A e. WOmni <-> A. f e. ( 2o ^m A )DECID A. x e. A ( f ` x ) = 1o ) )
98ibi 176 . . . . . . . 8 |- ( A e. WOmni -> A. f e. ( 2o ^m A )DECID A. x e. A ( f ` x ) = 1o )
109ad3antlr 497 . . . . . . 7 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> A. f e. ( 2o ^m A )DECID A. x e. A ( f ` x ) = 1o )
11 simpr 110 . . . . . . . . . . 11 |- ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) -> g e. ( 2o ^m B ) )
12 2onn 6794 . . . . . . . . . . . . 13 |- 2o e. om
13 relen 7026 . . . . . . . . . . . . . 14 |- Rel ~~
1413brrelex2i 4819 . . . . . . . . . . . . 13 |- ( A ~~ B -> B e. _V )
15 elmapg 6935 . . . . . . . . . . . . 13 |- ( ( 2o e. om /\ B e. _V ) -> ( g e. ( 2o ^m B ) <-> g : B --> 2o ) )
1612, 14, 15sylancr 418 . . . . . . . . . . . 12 |- ( A ~~ B -> ( g e. ( 2o ^m B ) <-> g : B --> 2o ) )
1716ad2antrr 492 . . . . . . . . . . 11 |- ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) -> ( g e. ( 2o ^m B ) <-> g : B --> 2o ) )
1811, 17mpbid 147 . . . . . . . . . 10 |- ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) -> g : B --> 2o )
1918adantr 276 . . . . . . . . 9 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> g : B --> 2o )
20 f1of 5639 . . . . . . . . . 10 |- ( h : A -1-1-onto-> B -> h : A --> B )
2120adantl 277 . . . . . . . . 9 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> h : A --> B )
22 fco 5552 . . . . . . . . 9 |- ( ( g : B --> 2o /\ h : A --> B ) -> ( g o. h ) : A --> 2o )
2319, 21, 22syl2anc 415 . . . . . . . 8 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> ( g o. h ) : A --> 2o )
24 simpllr 540 . . . . . . . . 9 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> A e. WOmni )
25 elmapg 6935 . . . . . . . . 9 |- ( ( 2o e. om /\ A e. WOmni ) -> ( ( g o. h ) e. ( 2o ^m A ) <-> ( g o. h ) : A --> 2o ) )
2612, 24, 25sylancr 418 . . . . . . . 8 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> ( ( g o. h ) e. ( 2o ^m A ) <-> ( g o. h ) : A --> 2o ) )
2723, 26mpbird 167 . . . . . . 7 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> ( g o. h ) e. ( 2o ^m A ) )
287, 10, 27rspcdva 2934 . . . . . 6 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> DECID A. x e. A ( ( g o. h ) ` x ) = 1o )
29 f1ofn 5640 . . . . . . . . . . . 12 |- ( h : A -1-1-onto-> B -> h Fn A )
3029ad3antlr 497 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> h Fn A )
31 f1ocnv 5652 . . . . . . . . . . . . . 14 |- ( h : A -1-1-onto-> B -> `' h : B -1-1-onto-> A )
32 f1of 5639 . . . . . . . . . . . . . 14 |- ( `' h : B -1-1-onto-> A -> `' h : B --> A )
3331, 32syl 14 . . . . . . . . . . . . 13 |- ( h : A -1-1-onto-> B -> `' h : B --> A )
3433ad3antlr 497 . . . . . . . . . . . 12 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> `' h : B --> A )
35 simpr 110 . . . . . . . . . . . 12 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> y e. B )
3634, 35ffvelcdmd 5844 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> ( `' h ` y ) e. A )
37 fvco2 5774 . . . . . . . . . . 11 |- ( ( h Fn A /\ ( `' h ` y ) e. A ) -> ( ( g o. h ) ` ( `' h ` y ) ) = ( g ` ( h ` ( `' h ` y ) ) ) )
3830, 36, 37syl2anc 415 . . . . . . . . . 10 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> ( ( g o. h ) ` ( `' h ` y ) ) = ( g ` ( h ` ( `' h ` y ) ) ) )
39 fveqeq2 5704 . . . . . . . . . . 11 |- ( x = ( `' h ` y ) -> ( ( ( g o. h ) ` x ) = 1o <-> ( ( g o. h ) ` ( `' h ` y ) ) = 1o ) )
40 simplr 533 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> A. x e. A ( ( g o. h ) ` x ) = 1o )
4139, 40, 36rspcdva 2934 . . . . . . . . . 10 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> ( ( g o. h ) ` ( `' h ` y ) ) = 1o )
42 f1ocnvfv2 5984 . . . . . . . . . . . 12 |- ( ( h : A -1-1-onto-> B /\ y e. B ) -> ( h ` ( `' h ` y ) ) = y )
4342fveq2d 5699 . . . . . . . . . . 11 |- ( ( h : A -1-1-onto-> B /\ y e. B ) -> ( g ` ( h ` ( `' h ` y ) ) ) = ( g ` y ) )
4443ad4ant24 520 . . . . . . . . . 10 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> ( g ` ( h ` ( `' h ` y ) ) ) = ( g ` y ) )
4538, 41, 443eqtr3rd 2280 . . . . . . . . 9 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) /\ y e. B ) -> ( g ` y ) = 1o )
4645ralrimiva 2623 . . . . . . . 8 |- ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. x e. A ( ( g o. h ) ` x ) = 1o ) -> A. y e. B ( g ` y ) = 1o )
4729ad3antlr 497 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> h Fn A )
48 simpr 110 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> x e. A )
49 fvco2 5774 . . . . . . . . . . 11 |- ( ( h Fn A /\ x e. A ) -> ( ( g o. h ) ` x ) = ( g ` ( h ` x ) ) )
5047, 48, 49syl2anc 415 . . . . . . . . . 10 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> ( ( g o. h ) ` x ) = ( g ` ( h ` x ) ) )
51 fveqeq2 5704 . . . . . . . . . . 11 |- ( y = ( h ` x ) -> ( ( g ` y ) = 1o <-> ( g ` ( h ` x ) ) = 1o ) )
52 simplr 533 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> A. y e. B ( g ` y ) = 1o )
5321ffvelcdmda 5843 . . . . . . . . . . . 12 |- ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ x e. A ) -> ( h ` x ) e. B )
5453adantlr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> ( h ` x ) e. B )
5551, 52, 54rspcdva 2934 . . . . . . . . . 10 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> ( g ` ( h ` x ) ) = 1o )
5650, 55eqtrd 2271 . . . . . . . . 9 |- ( ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) /\ x e. A ) -> ( ( g o. h ) ` x ) = 1o )
5756ralrimiva 2623 . . . . . . . 8 |- ( ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) /\ A. y e. B ( g ` y ) = 1o ) -> A. x e. A ( ( g o. h ) ` x ) = 1o )
5846, 57impbida 604 . . . . . . 7 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> ( A. x e. A ( ( g o. h ) ` x ) = 1o <-> A. y e. B ( g ` y ) = 1o ) )
5958dcbid 850 . . . . . 6 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> (DECID A. x e. A ( ( g o. h ) ` x ) = 1o <-> DECID A. y e. B ( g ` y ) = 1o ) )
6028, 59mpbid 147 . . . . 5 |- ( ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) /\ h : A -1-1-onto-> B ) -> DECID A. y e. B ( g ` y ) = 1o )
613, 60exlimddv 1954 . . . 4 |- ( ( ( A ~~ B /\ A e. WOmni ) /\ g e. ( 2o ^m B ) ) -> DECID A. y e. B ( g ` y ) = 1o )
6261ralrimiva 2623 . . 3 |- ( ( A ~~ B /\ A e. WOmni ) -> A. g e. ( 2o ^m B )DECID A. y e. B ( g ` y ) = 1o )
63 iswomnimap 7506 . . . . 5 |- ( B e. _V -> ( B e. WOmni <-> A. g e. ( 2o ^m B )DECID A. y e. B ( g ` y ) = 1o ) )
6414, 63syl 14 . . . 4 |- ( A ~~ B -> ( B e. WOmni <-> A. g e. ( 2o ^m B )DECID A. y e. B ( g ` y ) = 1o ) )
6564adantr 276 . . 3 |- ( ( A ~~ B /\ A e. WOmni ) -> ( B e. WOmni <-> A. g e. ( 2o ^m B )DECID A. y e. B ( g ` y ) = 1o ) )
6662, 65mpbird 167 . 2 |- ( ( A ~~ B /\ A e. WOmni ) -> B e. WOmni )
6766ex 115 1 |- ( A ~~ B -> ( A e. WOmni -> B e. WOmni ) )
Colors of variables:    wff set class
This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105  DECID wdc 846   = wceq 1402   E.wex 1545   e. wcel 2209   A.wral 2528   _Vcvv 2821   class class class wbr 4130   omcom 4737   `'ccnv 4773   o. ccom 4778   Fn wfn 5372   -->wf 5373   -1-1-onto->wf1o 5376   ` cfv 5377  (class class class)co 6085   1oc1o 6680   2oc2o 6681   ^m cmap 6922   ~~ cen 7020  WOmnicwomni 7503
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684
This proof depends on definitions:  df-bi 117  df-dc 847  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-id 4438  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1o 6687  df-2o 6688  df-map 6924  df-en 7023  df-womni 7504
This theorem is used by:  enwomni  7510
  Copyright terms: Public domain W3C validator