Metamath Proof Explorer

Theorem fin23lem22

Description: Lemma for fin23 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 ) between an infinite subset of _om and _om itself. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem22.b 
|- C = ( i e. _om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )
Assertion fin23lem22 
|- ( ( S C_ _om /\ -. S e. Fin ) -> C : _om -1-1-onto-> S )

Proof

Step Hyp Ref Expression
1 fin23lem22.b 
 |-  C = ( i e. _om |-> ( iota_ j e. S ( j i^i S ) ~~ i ) )
2 fin23lem23 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> E! j e. S ( j i^i S ) ~~ i )
3 riotacl 
 |-  ( E! j e. S ( j i^i S ) ~~ i -> ( iota_ j e. S ( j i^i S ) ~~ i ) e. S )
4 2 3 syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> ( iota_ j e. S ( j i^i S ) ~~ i ) e. S )
5 simpll 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ a e. S ) -> S C_ _om )
6 simpr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ a e. S ) -> a e. S )
7 5 6 sseldd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ a e. S ) -> a e. _om )
8 nnfi 
 |-  ( a e. _om -> a e. Fin )
9 infi 
 |-  ( a e. Fin -> ( a i^i S ) e. Fin )
10 ficardom 
 |-  ( ( a i^i S ) e. Fin -> ( card ` ( a i^i S ) ) e. _om )
11 7 8 9 10 4syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ a e. S ) -> ( card ` ( a i^i S ) ) e. _om )
12 cardnn 
 |-  ( i e. _om -> ( card ` i ) = i )
13 12 eqcomd 
 |-  ( i e. _om -> i = ( card ` i ) )
14 13 eqeq1d 
 |-  ( i e. _om -> ( i = ( card ` ( a i^i S ) ) <-> ( card ` i ) = ( card ` ( a i^i S ) ) ) )
15 eqcom 
 |-  ( ( card ` i ) = ( card ` ( a i^i S ) ) <-> ( card ` ( a i^i S ) ) = ( card ` i ) )
16 14 15 bitrdi 
 |-  ( i e. _om -> ( i = ( card ` ( a i^i S ) ) <-> ( card ` ( a i^i S ) ) = ( card ` i ) ) )
17 16 ad2antrl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( i = ( card ` ( a i^i S ) ) <-> ( card ` ( a i^i S ) ) = ( card ` i ) ) )
18 simpll 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> S C_ _om )
19 simprr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> a e. S )
20 18 19 sseldd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> a e. _om )
21 nnon 
 |-  ( a e. _om -> a e. On )
22 onenon 
 |-  ( a e. On -> a e. dom card )
23 20 21 22 3syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> a e. dom card )
24 inss1 
 |-  ( a i^i S ) C_ a
25 ssnum 
 |-  ( ( a e. dom card /\ ( a i^i S ) C_ a ) -> ( a i^i S ) e. dom card )
26 23 24 25 sylancl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( a i^i S ) e. dom card )
27 nnon 
 |-  ( i e. _om -> i e. On )
28 27 ad2antrl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> i e. On )
29 onenon 
 |-  ( i e. On -> i e. dom card )
30 28 29 syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> i e. dom card )
31 carden2 
 |-  ( ( ( a i^i S ) e. dom card /\ i e. dom card ) -> ( ( card ` ( a i^i S ) ) = ( card ` i ) <-> ( a i^i S ) ~~ i ) )
32 26 30 31 syl2anc 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( ( card ` ( a i^i S ) ) = ( card ` i ) <-> ( a i^i S ) ~~ i ) )
33 2 adantrr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> E! j e. S ( j i^i S ) ~~ i )
34 ineq1 
 |-  ( j = a -> ( j i^i S ) = ( a i^i S ) )
35 34 breq1d 
 |-  ( j = a -> ( ( j i^i S ) ~~ i <-> ( a i^i S ) ~~ i ) )
36 35 riota2 
 |-  ( ( a e. S /\ E! j e. S ( j i^i S ) ~~ i ) -> ( ( a i^i S ) ~~ i <-> ( iota_ j e. S ( j i^i S ) ~~ i ) = a ) )
37 19 33 36 syl2anc 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( ( a i^i S ) ~~ i <-> ( iota_ j e. S ( j i^i S ) ~~ i ) = a ) )
38 eqcom 
 |-  ( ( iota_ j e. S ( j i^i S ) ~~ i ) = a <-> a = ( iota_ j e. S ( j i^i S ) ~~ i ) )
39 37 38 bitrdi 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( ( a i^i S ) ~~ i <-> a = ( iota_ j e. S ( j i^i S ) ~~ i ) ) )
40 17 32 39 3bitrd 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ ( i e. _om /\ a e. S ) ) -> ( i = ( card ` ( a i^i S ) ) <-> a = ( iota_ j e. S ( j i^i S ) ~~ i ) ) )
41 1 4 11 40 f1o2d 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> C : _om -1-1-onto-> S )