Metamath Proof Explorer

Theorem fin23lem23

Description: Lemma for fin23lem22 . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem23 
|- ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> E! j e. S ( j i^i S ) ~~ i )

Proof

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 )