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 ) |