Metamath Proof Explorer

Theorem fin23lem27

Description: The mapping constructed in fin23lem22 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem22.b 
|- C = ( i e. _om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )
Assertion fin23lem27 
|- ( ( S C_ _om /\ -. S e. Fin ) -> C Isom _E , _E ( _om , S ) )

Proof

Step Hyp Ref Expression
1 fin23lem22.b 
 |-  C = ( i e. _om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )
2 ordom 
 |-  Ord _om
3 ordwe 
 |-  ( Ord _om -> _E We _om )
4 weso 
 |-  ( _E We _om -> _E Or _om )
5 2 3 4 mp2b 
 |-  _E Or _om
6 5 a1i 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> _E Or _om )
7 sopo 
 |-  ( _E Or _om -> _E Po _om )
8 5 7 ax-mp 
 |-  _E Po _om
9 poss 
 |-  ( S C_ _om -> ( _E Po _om -> _E Po S ) )
10 8 9 mpi 
 |-  ( S C_ _om -> _E Po S )
11 10 adantr 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> _E Po S )
12 1 fin23lem22 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> C : _om -1-1-onto-> S )
13 f1ofo 
 |-  ( C : _om -1-1-onto-> S -> C : _om -onto-> S )
14 12 13 syl 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> C : _om -onto-> S )
15 nnsdomel 
 |-  ( ( a e. _om /\ b e. _om ) -> ( a e. b <-> a ~< b ) )
16 15 adantl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a e. b <-> a ~< b ) )
17 16 biimpd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a e. b -> a ~< b ) )
18 fin23lem23 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ a e. _om ) -> E! j e. S ( j i^i S ) ~~ a )
19 18 adantrr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> E! j e. S ( j i^i S ) ~~ a )
20 ineq1 
 |-  ( j = i -> ( j i^i S ) = ( i i^i S ) )
21 20 breq1d 
 |-  ( j = i -> ( ( j i^i S ) ~~ a <-> ( i i^i S ) ~~ a ) )
22 21 cbvreuvw 
 |-  ( E! j e. S ( j i^i S ) ~~ a <-> E! i e. S ( i i^i S ) ~~ a )
23 19 22 sylib 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> E! i e. S ( i i^i S ) ~~ a )
24 nfv 
 |-  F/ i ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a
25 21 cbvriotavw 
 |-  ( iota_ j e. S ( j i^i S ) ~~ a ) = ( iota_ i e. S ( i i^i S ) ~~ a )
26 ineq1 
 |-  ( i = ( iota_ j e. S ( j i^i S ) ~~ a ) -> ( i i^i S ) = ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) )
27 26 breq1d 
 |-  ( i = ( iota_ j e. S ( j i^i S ) ~~ a ) -> ( ( i i^i S ) ~~ a <-> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a ) )
28 24 25 27 riotaprop 
 |-  ( E! i e. S ( i i^i S ) ~~ a -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) e. S /\ ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a ) )
29 23 28 syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) e. S /\ ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a ) )
30 29 simprd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a )
31 30 adantrr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( ( a e. _om /\ b e. _om ) /\ a ~< b ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a )
32 simprr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( ( a e. _om /\ b e. _om ) /\ a ~< b ) ) -> a ~< b )
33 fin23lem23 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ b e. _om ) -> E! j e. S ( j i^i S ) ~~ b )
34 33 adantrl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> E! j e. S ( j i^i S ) ~~ b )
35 20 breq1d 
 |-  ( j = i -> ( ( j i^i S ) ~~ b <-> ( i i^i S ) ~~ b ) )
36 35 cbvreuvw 
 |-  ( E! j e. S ( j i^i S ) ~~ b <-> E! i e. S ( i i^i S ) ~~ b )
37 34 36 sylib 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> E! i e. S ( i i^i S ) ~~ b )
38 nfv 
 |-  F/ i ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ~~ b
39 35 cbvriotavw 
 |-  ( iota_ j e. S ( j i^i S ) ~~ b ) = ( iota_ i e. S ( i i^i S ) ~~ b )
40 ineq1 
 |-  ( i = ( iota_ j e. S ( j i^i S ) ~~ b ) -> ( i i^i S ) = ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
41 40 breq1d 
 |-  ( i = ( iota_ j e. S ( j i^i S ) ~~ b ) -> ( ( i i^i S ) ~~ b <-> ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ~~ b ) )
42 38 39 41 riotaprop 
 |-  ( E! i e. S ( i i^i S ) ~~ b -> ( ( iota_ j e. S ( j i^i S ) ~~ b ) e. S /\ ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ~~ b ) )
43 37 42 syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ b ) e. S /\ ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ~~ b ) )
44 43 simprd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ~~ b )
45 44 ensymd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> b ~~ ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
46 45 adantrr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( ( a e. _om /\ b e. _om ) /\ a ~< b ) ) -> b ~~ ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
47 sdomentr 
 |-  ( ( a ~< b /\ b ~~ ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ) -> a ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
48 32 46 47 syl2anc 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( ( a e. _om /\ b e. _om ) /\ a ~< b ) ) -> a ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
49 ensdomtr 
 |-  ( ( ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~~ a /\ a ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
50 31 48 49 syl2anc 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( ( a e. _om /\ b e. _om ) /\ a ~< b ) ) -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) )
51 50 expr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a ~< b -> ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ) )
52 simpll 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> S C_ _om )
53 omsson 
 |-  _om C_ On
54 52 53 sstrdi 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> S C_ On )
55 29 simpld 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. S )
56 54 55 sseldd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. On )
57 43 simpld 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( iota_ j e. S ( j i^i S ) ~~ b ) e. S )
58 54 57 sseldd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( iota_ j e. S ( j i^i S ) ~~ b ) e. On )
59 onsdominel 
 |-  ( ( ( iota_ j e. S ( j i^i S ) ~~ a ) e. On /\ ( iota_ j e. S ( j i^i S ) ~~ b ) e. On /\ ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) ) -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. ( iota_ j e. S ( j i^i S ) ~~ b ) )
60 59 3expia 
 |-  ( ( ( iota_ j e. S ( j i^i S ) ~~ a ) e. On /\ ( iota_ j e. S ( j i^i S ) ~~ b ) e. On ) -> ( ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. ( iota_ j e. S ( j i^i S ) ~~ b ) ) )
61 56 58 60 syl2anc 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( ( iota_ j e. S ( j i^i S ) ~~ a ) i^i S ) ~< ( ( iota_ j e. S ( j i^i S ) ~~ b ) i^i S ) -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. ( iota_ j e. S ( j i^i S ) ~~ b ) ) )
62 17 51 61 3syld 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a e. b -> ( iota_ j e. S ( j i^i S ) ~~ a ) e. ( iota_ j e. S ( j i^i S ) ~~ b ) ) )
63 breq2 
 |-  ( i = a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ a ) )
64 63 riotabidv 
 |-  ( i = a -> ( iota_ j e. S ( j i^i S ) ~~ i ) = ( iota_ j e. S ( j i^i S ) ~~ a ) )
65 simprl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> a e. _om )
66 1 64 65 55 fvmptd3 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( C ` a ) = ( iota_ j e. S ( j i^i S ) ~~ a ) )
67 breq2 
 |-  ( i = b -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ b ) )
68 67 riotabidv 
 |-  ( i = b -> ( iota_ j e. S ( j i^i S ) ~~ i ) = ( iota_ j e. S ( j i^i S ) ~~ b ) )
69 simprr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> b e. _om )
70 1 68 69 57 fvmptd3 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( C ` b ) = ( iota_ j e. S ( j i^i S ) ~~ b ) )
71 66 70 eleq12d 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( C ` a ) e. ( C ` b ) <-> ( iota_ j e. S ( j i^i S ) ~~ a ) e. ( iota_ j e. S ( j i^i S ) ~~ b ) ) )
72 62 71 sylibrd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a e. b -> ( C ` a ) e. ( C ` b ) ) )
73 epel 
 |-  ( a _E b <-> a e. b )
74 fvex 
 |-  ( C ` b ) e. _V
75 74 epeli 
 |-  ( ( C ` a ) _E ( C ` b ) <-> ( C ` a ) e. ( C ` b ) )
76 72 73 75 3imtr4g 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( a e. _om /\ b e. _om ) ) -> ( a _E b -> ( C ` a ) _E ( C ` b ) ) )
77 76 ralrimivva 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> A. a e. _om A. b e. _om ( a _E b -> ( C ` a ) _E ( C ` b ) ) )
78 soisoi 
 |-  ( ( ( _E Or _om /\ _E Po S ) /\ ( C : _om -onto-> S /\ A. a e. _om A. b e. _om ( a _E b -> ( C ` a ) _E ( C ` b ) ) ) ) -> C Isom _E , _E ( _om , S ) )
79 6 11 14 77 78 syl22anc 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> C Isom _E , _E ( _om , S ) )