Metamath Proof Explorer

Theorem fin23lem26

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

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

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( i = (/) -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ (/) ) )
2 1 rexbidv 
 |-  ( i = (/) -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ (/) ) )
3 breq2 
 |-  ( i = a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ a ) )
4 3 rexbidv 
 |-  ( i = a -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ a ) )
5 breq2 
 |-  ( i = suc a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ suc a ) )
6 5 rexbidv 
 |-  ( i = suc a -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ suc a ) )
7 ordom 
 |-  Ord _om
8 simpl 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> S C_ _om )
9 0fin 
 |-  (/) e. Fin
10 eleq1 
 |-  ( S = (/) -> ( S e. Fin <-> (/) e. Fin ) )
11 9 10 mpbiri 
 |-  ( S = (/) -> S e. Fin )
12 11 necon3bi 
 |-  ( -. S e. Fin -> S =/= (/) )
13 12 adantl 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> S =/= (/) )
14 tz7.5 
 |-  ( ( Ord _om /\ S C_ _om /\ S =/= (/) ) -> E. j e. S ( S i^i j ) = (/) )
15 7 8 13 14 mp3an2i 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> E. j e. S ( S i^i j ) = (/) )
16 en0 
 |-  ( ( j i^i S ) ~~ (/) <-> ( j i^i S ) = (/) )
17 incom 
 |-  ( j i^i S ) = ( S i^i j )
18 17 eqeq1i 
 |-  ( ( j i^i S ) = (/) <-> ( S i^i j ) = (/) )
19 16 18 bitri 
 |-  ( ( j i^i S ) ~~ (/) <-> ( S i^i j ) = (/) )
20 19 rexbii 
 |-  ( E. j e. S ( j i^i S ) ~~ (/) <-> E. j e. S ( S i^i j ) = (/) )
21 15 20 sylibr 
 |-  ( ( S C_ _om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ (/) )
22 simplrl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ _om )
23 omsson 
 |-  _om C_ On
24 22 23 sstrdi 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ On )
25 24 ssdifssd 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( S \ suc j ) C_ On )
26 simplr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ j e. S ) -> -. S e. Fin )
27 ssel2 
 |-  ( ( S C_ _om /\ j e. S ) -> j e. _om )
28 onfin2 
 |-  _om = ( On i^i Fin )
29 inss2 
 |-  ( On i^i Fin ) C_ Fin
30 28 29 eqsstri 
 |-  _om C_ Fin
31 peano2 
 |-  ( j e. _om -> suc j e. _om )
32 30 31 sseldi 
 |-  ( j e. _om -> suc j e. Fin )
33 27 32 syl 
 |-  ( ( S C_ _om /\ j e. S ) -> suc j e. Fin )
34 33 adantlr 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ j e. S ) -> suc j e. Fin )
35 ssfi 
 |-  ( ( suc j e. Fin /\ S C_ suc j ) -> S e. Fin )
36 35 ex 
 |-  ( suc j e. Fin -> ( S C_ suc j -> S e. Fin ) )
37 34 36 syl 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ j e. S ) -> ( S C_ suc j -> S e. Fin ) )
38 26 37 mtod 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ j e. S ) -> -. S C_ suc j )
39 ssdif0 
 |-  ( S C_ suc j <-> ( S \ suc j ) = (/) )
40 39 necon3bbii 
 |-  ( -. S C_ suc j <-> ( S \ suc j ) =/= (/) )
41 38 40 sylib 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ j e. S ) -> ( S \ suc j ) =/= (/) )
42 41 ad2ant2lr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( S \ suc j ) =/= (/) )
43 onint 
 |-  ( ( ( S \ suc j ) C_ On /\ ( S \ suc j ) =/= (/) ) -> |^| ( S \ suc j ) e. ( S \ suc j ) )
44 25 42 43 syl2anc 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> |^| ( S \ suc j ) e. ( S \ suc j ) )
45 44 eldifad 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> |^| ( S \ suc j ) e. S )
46 simprr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( j i^i S ) ~~ a )
47 en2sn 
 |-  ( ( j e. _V /\ a e. _V ) -> { j } ~~ { a } )
48 47 el2v 
 |-  { j } ~~ { a }
49 48 a1i 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> { j } ~~ { a } )
50 simprl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. S )
51 22 50 sseldd 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. _om )
52 nnord 
 |-  ( j e. _om -> Ord j )
53 51 52 syl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> Ord j )
54 ordirr 
 |-  ( Ord j -> -. j e. j )
55 elinel1 
 |-  ( j e. ( j i^i S ) -> j e. j )
56 54 55 nsyl 
 |-  ( Ord j -> -. j e. ( j i^i S ) )
57 disjsn 
 |-  ( ( ( j i^i S ) i^i { j } ) = (/) <-> -. j e. ( j i^i S ) )
58 56 57 sylibr 
 |-  ( Ord j -> ( ( j i^i S ) i^i { j } ) = (/) )
59 53 58 syl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( ( j i^i S ) i^i { j } ) = (/) )
60 nnord 
 |-  ( a e. _om -> Ord a )
61 ordirr 
 |-  ( Ord a -> -. a e. a )
62 60 61 syl 
 |-  ( a e. _om -> -. a e. a )
63 disjsn 
 |-  ( ( a i^i { a } ) = (/) <-> -. a e. a )
64 62 63 sylibr 
 |-  ( a e. _om -> ( a i^i { a } ) = (/) )
65 64 ad2antrr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( a i^i { a } ) = (/) )
66 unen 
 |-  ( ( ( ( j i^i S ) ~~ a /\ { j } ~~ { a } ) /\ ( ( ( j i^i S ) i^i { j } ) = (/) /\ ( a i^i { a } ) = (/) ) ) -> ( ( j i^i S ) u. { j } ) ~~ ( a u. { a } ) )
67 46 49 59 65 66 syl22anc 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( ( j i^i S ) u. { j } ) ~~ ( a u. { a } ) )
68 simprr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> b e. S )
69 simplrl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> S C_ _om )
70 69 23 sstrdi 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> S C_ On )
71 ordsuc 
 |-  ( Ord j <-> Ord suc j )
72 53 71 sylib 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> Ord suc j )
73 72 adantrr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> Ord suc j )
74 simp2 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> S C_ On )
75 74 ssdifssd 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( S \ suc j ) C_ On )
76 simpl1 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. S )
77 simpr 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> -. b e. suc j )
78 76 77 eldifd 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. ( S \ suc j ) )
79 78 ex 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> b e. ( S \ suc j ) ) )
80 onnmin 
 |-  ( ( ( S \ suc j ) C_ On /\ b e. ( S \ suc j ) ) -> -. b e. |^| ( S \ suc j ) )
81 75 79 80 syl6an 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> -. b e. |^| ( S \ suc j ) ) )
82 81 con4d 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) -> b e. suc j ) )
83 82 imp 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. |^| ( S \ suc j ) ) -> b e. suc j )
84 simp3 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> Ord suc j )
85 ordsucss 
 |-  ( Ord suc j -> ( b e. suc j -> suc b C_ suc j ) )
86 84 85 syl 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. suc j -> suc b C_ suc j ) )
87 86 imp 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> suc b C_ suc j )
88 87 sscond 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> ( S \ suc j ) C_ ( S \ suc b ) )
89 intss 
 |-  ( ( S \ suc j ) C_ ( S \ suc b ) -> |^| ( S \ suc b ) C_ |^| ( S \ suc j ) )
90 88 89 syl 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> |^| ( S \ suc b ) C_ |^| ( S \ suc j ) )
91 simpl2 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> S C_ On )
92 ordelon 
 |-  ( ( Ord suc j /\ b e. suc j ) -> b e. On )
93 84 92 sylan 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. On )
94 onmindif 
 |-  ( ( S C_ On /\ b e. On ) -> b e. |^| ( S \ suc b ) )
95 91 93 94 syl2anc 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc b ) )
96 90 95 sseldd 
 |-  ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc j ) )
97 83 96 impbida 
 |-  ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) <-> b e. suc j ) )
98 68 70 73 97 syl3anc 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> ( b e. |^| ( S \ suc j ) <-> b e. suc j ) )
99 df-suc 
 |-  suc j = ( j u. { j } )
100 99 eleq2i 
 |-  ( b e. suc j <-> b e. ( j u. { j } ) )
101 98 100 bitrdi 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> ( b e. |^| ( S \ suc j ) <-> b e. ( j u. { j } ) ) )
102 101 expr 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( b e. S -> ( b e. |^| ( S \ suc j ) <-> b e. ( j u. { j } ) ) ) )
103 102 pm5.32rd 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( ( b e. |^| ( S \ suc j ) /\ b e. S ) <-> ( b e. ( j u. { j } ) /\ b e. S ) ) )
104 elin 
 |-  ( b e. ( |^| ( S \ suc j ) i^i S ) <-> ( b e. |^| ( S \ suc j ) /\ b e. S ) )
105 elin 
 |-  ( b e. ( ( j u. { j } ) i^i S ) <-> ( b e. ( j u. { j } ) /\ b e. S ) )
106 103 104 105 3bitr4g 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( b e. ( |^| ( S \ suc j ) i^i S ) <-> b e. ( ( j u. { j } ) i^i S ) ) )
107 106 eqrdv 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( |^| ( S \ suc j ) i^i S ) = ( ( j u. { j } ) i^i S ) )
108 indir 
 |-  ( ( j u. { j } ) i^i S ) = ( ( j i^i S ) u. ( { j } i^i S ) )
109 107 108 eqtrdi 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( |^| ( S \ suc j ) i^i S ) = ( ( j i^i S ) u. ( { j } i^i S ) ) )
110 snssi 
 |-  ( j e. S -> { j } C_ S )
111 df-ss 
 |-  ( { j } C_ S <-> ( { j } i^i S ) = { j } )
112 110 111 sylib 
 |-  ( j e. S -> ( { j } i^i S ) = { j } )
113 112 uneq2d 
 |-  ( j e. S -> ( ( j i^i S ) u. ( { j } i^i S ) ) = ( ( j i^i S ) u. { j } ) )
114 113 ad2antrl 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( ( j i^i S ) u. ( { j } i^i S ) ) = ( ( j i^i S ) u. { j } ) )
115 109 114 eqtrd 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( |^| ( S \ suc j ) i^i S ) = ( ( j i^i S ) u. { j } ) )
116 df-suc 
 |-  suc a = ( a u. { a } )
117 116 a1i 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> suc a = ( a u. { a } ) )
118 67 115 117 3brtr4d 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( |^| ( S \ suc j ) i^i S ) ~~ suc a )
119 ineq1 
 |-  ( b = |^| ( S \ suc j ) -> ( b i^i S ) = ( |^| ( S \ suc j ) i^i S ) )
120 119 breq1d 
 |-  ( b = |^| ( S \ suc j ) -> ( ( b i^i S ) ~~ suc a <-> ( |^| ( S \ suc j ) i^i S ) ~~ suc a ) )
121 120 rspcev 
 |-  ( ( |^| ( S \ suc j ) e. S /\ ( |^| ( S \ suc j ) i^i S ) ~~ suc a ) -> E. b e. S ( b i^i S ) ~~ suc a )
122 45 118 121 syl2anc 
 |-  ( ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> E. b e. S ( b i^i S ) ~~ suc a )
123 122 rexlimdvaa 
 |-  ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) -> ( E. j e. S ( j i^i S ) ~~ a -> E. b e. S ( b i^i S ) ~~ suc a ) )
124 ineq1 
 |-  ( b = j -> ( b i^i S ) = ( j i^i S ) )
125 124 breq1d 
 |-  ( b = j -> ( ( b i^i S ) ~~ suc a <-> ( j i^i S ) ~~ suc a ) )
126 125 cbvrexvw 
 |-  ( E. b e. S ( b i^i S ) ~~ suc a <-> E. j e. S ( j i^i S ) ~~ suc a )
127 123 126 syl6ib 
 |-  ( ( a e. _om /\ ( S C_ _om /\ -. S e. Fin ) ) -> ( E. j e. S ( j i^i S ) ~~ a -> E. j e. S ( j i^i S ) ~~ suc a ) )
128 127 ex 
 |-  ( a e. _om -> ( ( S C_ _om /\ -. S e. Fin ) -> ( E. j e. S ( j i^i S ) ~~ a -> E. j e. S ( j i^i S ) ~~ suc a ) ) )
129 2 4 6 21 128 finds2 
 |-  ( i e. _om -> ( ( S C_ _om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ i ) )
130 129 impcom 
 |-  ( ( ( S C_ _om /\ -. S e. Fin ) /\ i e. _om ) -> E. j e. S ( j i^i S ) ~~ i )