| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fin23lem26 |
|- ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> E. j e. S ( j i^i S ) ~~ i ) |
| 2 |
|
ensym |
|- ( ( a i^i S ) ~~ i -> i ~~ ( a i^i S ) ) |
| 3 |
|
entr |
|- ( ( ( j i^i S ) ~~ i /\ i ~~ ( a i^i S ) ) -> ( j i^i S ) ~~ ( a i^i S ) ) |
| 4 |
2 3
|
sylan2 |
|- ( ( ( j i^i S ) ~~ i /\ ( a i^i S ) ~~ i ) -> ( j i^i S ) ~~ ( a i^i S ) ) |
| 5 |
|
simpl |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> S C_ _om ) |
| 6 |
|
simprl |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> j e. S ) |
| 7 |
5 6
|
sseldd |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> j e. _om ) |
| 8 |
|
nnfi |
|- ( j e. _om -> j e. Fin ) |
| 9 |
|
inss1 |
|- ( j i^i S ) C_ j |
| 10 |
|
ssfi |
|- ( ( j e. Fin /\ ( j i^i S ) C_ j ) -> ( j i^i S ) e. Fin ) |
| 11 |
8 9 10
|
sylancl |
|- ( j e. _om -> ( j i^i S ) e. Fin ) |
| 12 |
7 11
|
syl |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( j i^i S ) e. Fin ) |
| 13 |
|
simprr |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> a e. S ) |
| 14 |
5 13
|
sseldd |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> a e. _om ) |
| 15 |
|
nnfi |
|- ( a e. _om -> a e. Fin ) |
| 16 |
|
inss1 |
|- ( a i^i S ) C_ a |
| 17 |
|
ssfi |
|- ( ( a e. Fin /\ ( a i^i S ) C_ a ) -> ( a i^i S ) e. Fin ) |
| 18 |
15 16 17
|
sylancl |
|- ( a e. _om -> ( a i^i S ) e. Fin ) |
| 19 |
14 18
|
syl |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( a i^i S ) e. Fin ) |
| 20 |
|
nnord |
|- ( j e. _om -> Ord j ) |
| 21 |
|
nnord |
|- ( a e. _om -> Ord a ) |
| 22 |
|
ordtri2or2 |
|- ( ( Ord j /\ Ord a ) -> ( j C_ a \/ a C_ j ) ) |
| 23 |
20 21 22
|
syl2an |
|- ( ( j e. _om /\ a e. _om ) -> ( j C_ a \/ a C_ j ) ) |
| 24 |
7 14 23
|
syl2anc |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( j C_ a \/ a C_ j ) ) |
| 25 |
|
ssrin |
|- ( j C_ a -> ( j i^i S ) C_ ( a i^i S ) ) |
| 26 |
|
ssrin |
|- ( a C_ j -> ( a i^i S ) C_ ( j i^i S ) ) |
| 27 |
25 26
|
orim12i |
|- ( ( j C_ a \/ a C_ j ) -> ( ( j i^i S ) C_ ( a i^i S ) \/ ( a i^i S ) C_ ( j i^i S ) ) ) |
| 28 |
24 27
|
syl |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( ( j i^i S ) C_ ( a i^i S ) \/ ( a i^i S ) C_ ( j i^i S ) ) ) |
| 29 |
|
fin23lem25 |
|- ( ( ( j i^i S ) e. Fin /\ ( a i^i S ) e. Fin /\ ( ( j i^i S ) C_ ( a i^i S ) \/ ( a i^i S ) C_ ( j i^i S ) ) ) -> ( ( j i^i S ) ~~ ( a i^i S ) <-> ( j i^i S ) = ( a i^i S ) ) ) |
| 30 |
12 19 28 29
|
syl3anc |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( ( j i^i S ) ~~ ( a i^i S ) <-> ( j i^i S ) = ( a i^i S ) ) ) |
| 31 |
|
ordom |
|- Ord _om |
| 32 |
|
fin23lem24 |
|- ( ( ( Ord _om /\ S C_ _om ) /\ ( j e. S /\ a e. S ) ) -> ( ( j i^i S ) = ( a i^i S ) <-> j = a ) ) |
| 33 |
31 32
|
mpanl1 |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( ( j i^i S ) = ( a i^i S ) <-> j = a ) ) |
| 34 |
30 33
|
bitrd |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( ( j i^i S ) ~~ ( a i^i S ) <-> j = a ) ) |
| 35 |
4 34
|
imbitrid |
|- ( ( S C_ _om /\ ( j e. S /\ a e. S ) ) -> ( ( ( j i^i S ) ~~ i /\ ( a i^i S ) ~~ i ) -> j = a ) ) |
| 36 |
35
|
ralrimivva |
|- ( S C_ _om -> A. j e. S A. a e. S ( ( ( j i^i S ) ~~ i /\ ( a i^i S ) ~~ i ) -> j = a ) ) |
| 37 |
36
|
ad2antrr |
|- ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> A. j e. S A. a e. S ( ( ( j i^i S ) ~~ i /\ ( a i^i S ) ~~ i ) -> j = a ) ) |
| 38 |
|
ineq1 |
|- ( j = a -> ( j i^i S ) = ( a i^i S ) ) |
| 39 |
38
|
breq1d |
|- ( j = a -> ( ( j i^i S ) ~~ i <-> ( a i^i S ) ~~ i ) ) |
| 40 |
39
|
reu4 |
|- ( E! j e. S ( j i^i S ) ~~ i <-> ( E. j e. S ( j i^i S ) ~~ i /\ A. j e. S A. a e. S ( ( ( j i^i S ) ~~ i /\ ( a i^i S ) ~~ i ) -> j = a ) ) ) |
| 41 |
1 37 40
|
sylanbrc |
|- ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> E! j e. S ( j i^i S ) ~~ i ) |