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 )