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