MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin23lem26 Structured version   Visualization version   Unicode version
Theorem fin23lem26 9147
Description: Lemma for fin23lem22 9149. (Contributed by Stefan O'Rear, 1-Nov-2014.)
Assertion
Ref Expression
fin23lem26 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ i e. om ) -> E. j e. S ( j i^i S ) ~~ i )
Distinct variable group:   i, j, S
Proof of Theorem fin23lem26
Dummy variables a b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4657 . . . 4 |- ( i = (/) -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ (/) ) )
21rexbidv 3052 . . 3 |- ( i = (/) -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ (/) ) )
3 breq2 4657 . . . 4 |- ( i = a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ a ) )
43rexbidv 3052 . . 3 |- ( i = a -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ a ) )
5 breq2 4657 . . . 4 |- ( i = suc a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ suc a ) )
65rexbidv 3052 . . 3 |- ( i = suc a -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ suc a ) )
7 ordom 7074 . . . . . 6 |- Ord om
87a1i 11 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> Ord om )
9 simpl 473 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> S C_ om )
10 0fin 8188 . . . . . . . 8 |- (/) e. Fin
11 eleq1 2689 . . . . . . . 8 |- ( S = (/) -> ( S e. Fin <-> (/) e. Fin ) )
1210, 11mpbiri 248 . . . . . . 7 |- ( S = (/) -> S e. Fin )
1312necon3bi 2820 . . . . . 6 |- ( -. S e. Fin -> S =/= (/) )
1413adantl 482 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> S =/= (/) )
15 tz7.5 5744 . . . . 5 |- ( ( Ord om /\ S C_ om /\ S =/= (/) ) -> E. j e. S ( S i^i j ) = (/) )
168, 9, 14, 15syl3anc 1326 . . . 4 |- ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( S i^i j ) = (/) )
17 en0 8019 . . . . . 6 |- ( ( j i^i S ) ~~ (/) <-> ( j i^i S ) = (/) )
18 incom 3805 . . . . . . 7 |- ( j i^i S ) = ( S i^i j )
1918eqeq1i 2627 . . . . . 6 |- ( ( j i^i S ) = (/) <-> ( S i^i j ) = (/) )
2017, 19bitri 264 . . . . 5 |- ( ( j i^i S ) ~~ (/) <-> ( S i^i j ) = (/) )
2120rexbii 3041 . . . 4 |- ( E. j e. S ( j i^i S ) ~~ (/) <-> E. j e. S ( S i^i j ) = (/) )
2216, 21sylibr 224 . . 3 |- ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ (/) )
23 simplrl 800 . . . . . . . . . . 11 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ om )
24 omsson 7069 . . . . . . . . . . 11 |- om C_ On
2523, 24syl6ss 3615 . . . . . . . . . 10 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ On )
2625ssdifssd 3748 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( S \ suc j ) C_ On )
27 simplr 792 . . . . . . . . . . . 12 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> -. S e. Fin )
28 ssel2 3598 . . . . . . . . . . . . . . 15 |- ( ( S C_ om /\ j e. S ) -> j e. om )
29 onfin2 8152 . . . . . . . . . . . . . . . . 17 |- om = ( On i^i Fin )
30 inss2 3834 . . . . . . . . . . . . . . . . 17 |- ( On i^i Fin ) C_ Fin
3129, 30eqsstri 3635 . . . . . . . . . . . . . . . 16 |- om C_ Fin
32 peano2 7086 . . . . . . . . . . . . . . . 16 |- ( j e. om -> suc j e. om )
3331, 32sseldi 3601 . . . . . . . . . . . . . . 15 |- ( j e. om -> suc j e. Fin )
3428, 33syl 17 . . . . . . . . . . . . . 14 |- ( ( S C_ om /\ j e. S ) -> suc j e. Fin )
3534adantlr 751 . . . . . . . . . . . . 13 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> suc j e. Fin )
36 ssfi 8180 . . . . . . . . . . . . . 14 |- ( ( suc j e. Fin /\ S C_ suc j ) -> S e. Fin )
3736ex 450 . . . . . . . . . . . . 13 |- ( suc j e. Fin -> ( S C_ suc j -> S e. Fin ) )
3835, 37syl 17 . . . . . . . . . . . 12 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> ( S C_ suc j -> S e. Fin ) )
3927, 38mtod 189 . . . . . . . . . . 11 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> -. S C_ suc j )
40 ssdif0 3942 . . . . . . . . . . . 12 |- ( S C_ suc j <-> ( S \ suc j ) = (/) )
4140necon3bbii 2841 . . . . . . . . . . 11 |- ( -. S C_ suc j <-> ( S \ suc j ) =/= (/) )
4239, 41sylib 208 . . . . . . . . . 10 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> ( S \ suc j ) =/= (/) )
4342ad2ant2lr 784 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( S \ suc j ) =/= (/) )
44 onint 6995 . . . . . . . . 9 |- ( ( ( S \ suc j ) C_ On /\ ( S \ suc j ) =/= (/) ) -> |^| ( S \ suc j ) e. ( S \ suc j ) )
4526, 43, 44syl2anc 693 . . . . . . . 8 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> |^| ( S \ suc j ) e. ( S \ suc j ) )
4645eldifad 3586 . . . . . . 7 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> |^| ( S \ suc j ) e. S )
47 simprr 796 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( j i^i S ) ~~ a )
48 vex 3203 . . . . . . . . . . 11 |- j e. _V
49 vex 3203 . . . . . . . . . . 11 |- a e. _V
50 en2sn 8037 . . . . . . . . . . 11 |- ( ( j e. _V /\ a e. _V ) -> { j } ~~ { a } )
5148, 49, 50mp2an 708 . . . . . . . . . 10 |- { j } ~~ { a }
5251a1i 11 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> { j } ~~ { a } )
53 simprl 794 . . . . . . . . . . . 12 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. S )
5423, 53sseldd 3604 . . . . . . . . . . 11 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. om )
55 nnord 7073 . . . . . . . . . . 11 |- ( j e. om -> Ord j )
5654, 55syl 17 . . . . . . . . . 10 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> Ord j )
57 ordirr 5741 . . . . . . . . . . . 12 |- ( Ord j -> -. j e. j )
58 inss1 3833 . . . . . . . . . . . . 13 |- ( j i^i S ) C_ j
5958sseli 3599 . . . . . . . . . . . 12 |- ( j e. ( j i^i S ) -> j e. j )
6057, 59nsyl 135 . . . . . . . . . . 11 |- ( Ord j -> -. j e. ( j i^i S ) )
61 disjsn 4246 . . . . . . . . . . 11 |- ( ( ( j i^i S ) i^i { j } ) = (/) <-> -. j e. ( j i^i S ) )
6260, 61sylibr 224 . . . . . . . . . 10 |- ( Ord j -> ( ( j i^i S ) i^i { j } ) = (/) )
6356, 62syl 17 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( ( j i^i S ) i^i { j } ) = (/) )
64 nnord 7073 . . . . . . . . . . . 12 |- ( a e. om -> Ord a )
65 ordirr 5741 . . . . . . . . . . . 12 |- ( Ord a -> -. a e. a )
6664, 65syl 17 . . . . . . . . . . 11 |- ( a e. om -> -. a e. a )
67 disjsn 4246 . . . . . . . . . . 11 |- ( ( a i^i { a } ) = (/) <-> -. a e. a )
6866, 67sylibr 224 . . . . . . . . . 10 |- ( a e. om -> ( a i^i { a } ) = (/) )
6968ad2antrr 762 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( a i^i { a } ) = (/) )
70 unen 8040 . . . . . . . . 9 |- ( ( ( ( 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 } ) )
7147, 52, 63, 69, 70syl22anc 1327 . . . . . . . 8 |- ( ( ( 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 } ) )
72 simprr 796 . . . . . . . . . . . . . . . 16 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> b e. S )
73 simplrl 800 . . . . . . . . . . . . . . . . 17 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> S C_ om )
7473, 24syl6ss 3615 . . . . . . . . . . . . . . . 16 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> S C_ On )
75 ordsuc 7014 . . . . . . . . . . . . . . . . . 18 |- ( Ord j <-> Ord suc j )
7656, 75sylib 208 . . . . . . . . . . . . . . . . 17 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> Ord suc j )
7776adantrr 753 . . . . . . . . . . . . . . . 16 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( ( j e. S /\ ( j i^i S ) ~~ a ) /\ b e. S ) ) -> Ord suc j )
78 simp2 1062 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> S C_ On )
7978ssdifssd 3748 . . . . . . . . . . . . . . . . . . . 20 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( S \ suc j ) C_ On )
80 simpl1 1064 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. S )
81 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> -. b e. suc j )
8280, 81eldifd 3585 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. ( S \ suc j ) )
8382ex 450 . . . . . . . . . . . . . . . . . . . 20 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> b e. ( S \ suc j ) ) )
84 onnmin 7003 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( S \ suc j ) C_ On /\ b e. ( S \ suc j ) ) -> -. b e. |^| ( S \ suc j ) )
8579, 83, 84syl6an 568 . . . . . . . . . . . . . . . . . . 19 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> -. b e. |^| ( S \ suc j ) ) )
8685con4d 114 . . . . . . . . . . . . . . . . . 18 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) -> b e. suc j ) )
8786imp 445 . . . . . . . . . . . . . . . . 17 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. |^| ( S \ suc j ) ) -> b e. suc j )
88 simp3 1063 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> Ord suc j )
89 ordsucss 7018 . . . . . . . . . . . . . . . . . . . . . 22 |- ( Ord suc j -> ( b e. suc j -> suc b C_ suc j ) )
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. suc j -> suc b C_ suc j ) )
9190imp 445 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> suc b C_ suc j )
9291sscond 3747 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> ( S \ suc j ) C_ ( S \ suc b ) )
93 intss 4498 . . . . . . . . . . . . . . . . . . 19 |- ( ( S \ suc j ) C_ ( S \ suc b ) -> |^| ( S \ suc b ) C_ |^| ( S \ suc j ) )
9492, 93syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> |^| ( S \ suc b ) C_ |^| ( S \ suc j ) )
95 simpl2 1065 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> S C_ On )
96 ordelon 5747 . . . . . . . . . . . . . . . . . . . 20 |- ( ( Ord suc j /\ b e. suc j ) -> b e. On )
9788, 96sylan 488 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. On )
98 onmindif 5815 . . . . . . . . . . . . . . . . . . 19 |- ( ( S C_ On /\ b e. On ) -> b e. |^| ( S \ suc b ) )
9995, 97, 98syl2anc 693 . . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc b ) )
10094, 99sseldd 3604 . . . . . . . . . . . . . . . . 17 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc j ) )
10187, 100impbida 877 . . . . . . . . . . . . . . . 16 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) <-> b e. suc j ) )
10272, 74, 77, 101syl3anc 1326 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
103 df-suc 5729 . . . . . . . . . . . . . . . 16 |- suc j = ( j u. { j } )
104103eleq2i 2693 . . . . . . . . . . . . . . 15 |- ( b e. suc j <-> b e. ( j u. { j } ) )
105102, 104syl6bb 276 . . . . . . . . . . . . . 14 |- ( ( ( 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 } ) ) )
106105expr 643 . . . . . . . . . . . . 13 |- ( ( ( 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 } ) ) ) )
107106pm5.32rd 672 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
108 elin 3796 . . . . . . . . . . . 12 |- ( b e. ( |^| ( S \ suc j ) i^i S ) <-> ( b e. |^| ( S \ suc j ) /\ b e. S ) )
109 elin 3796 . . . . . . . . . . . 12 |- ( b e. ( ( j u. { j } ) i^i S ) <-> ( b e. ( j u. { j } ) /\ b e. S ) )
110107, 108, 1093bitr4g 303 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
111110eqrdv 2620 . . . . . . . . . 10 |- ( ( ( 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 ) )
112 indir 3875 . . . . . . . . . 10 |- ( ( j u. { j } ) i^i S ) = ( ( j i^i S ) u. ( { j } i^i S ) )
113111, 112syl6eq 2672 . . . . . . . . 9 |- ( ( ( 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 ) ) )
114 snssi 4339 . . . . . . . . . . . 12 |- ( j e. S -> { j } C_ S )
115 df-ss 3588 . . . . . . . . . . . 12 |- ( { j } C_ S <-> ( { j } i^i S ) = { j } )
116114, 115sylib 208 . . . . . . . . . . 11 |- ( j e. S -> ( { j } i^i S ) = { j } )
117116uneq2d 3767 . . . . . . . . . 10 |- ( j e. S -> ( ( j i^i S ) u. ( { j } i^i S ) ) = ( ( j i^i S ) u. { j } ) )
118117ad2antrl 764 . . . . . . . . 9 |- ( ( ( 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 } ) )
119113, 118eqtrd 2656 . . . . . . . 8 |- ( ( ( 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 } ) )
120 df-suc 5729 . . . . . . . . 9 |- suc a = ( a u. { a } )
121120a1i 11 . . . . . . . 8 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> suc a = ( a u. { a } ) )
12271, 119, 1213brtr4d 4685 . . . . . . 7 |- ( ( ( 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 )
123 ineq1 3807 . . . . . . . . 9 |- ( b = |^| ( S \ suc j ) -> ( b i^i S ) = ( |^| ( S \ suc j ) i^i S ) )
124123breq1d 4663 . . . . . . . 8 |- ( b = |^| ( S \ suc j ) -> ( ( b i^i S ) ~~ suc a <-> ( |^| ( S \ suc j ) i^i S ) ~~ suc a ) )
125124rspcev 3309 . . . . . . 7 |- ( ( |^| ( S \ suc j ) e. S /\ ( |^| ( S \ suc j ) i^i S ) ~~ suc a ) -> E. b e. S ( b i^i S ) ~~ suc a )
12646, 122, 125syl2anc 693 . . . . . 6 |- ( ( ( 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 )
127126rexlimdvaa 3032 . . . . 5 |- ( ( 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 ) )
128 ineq1 3807 . . . . . . 7 |- ( b = j -> ( b i^i S ) = ( j i^i S ) )
129128breq1d 4663 . . . . . 6 |- ( b = j -> ( ( b i^i S ) ~~ suc a <-> ( j i^i S ) ~~ suc a ) )
130129cbvrexv 3172 . . . . 5 |- ( E. b e. S ( b i^i S ) ~~ suc a <-> E. j e. S ( j i^i S ) ~~ suc a )
131127, 130syl6ib 241 . . . 4 |- ( ( 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 ) )
132131ex 450 . . 3 |- ( 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 ) ) )
1332, 4, 6, 22, 132finds2 7094 . 2 |- ( i e. om -> ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ i ) )
134133impcom 446 1 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ i e. om ) -> E. j e. S ( j i^i S ) ~~ i )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   |^|cint 4475   class class class wbr 4653   Ord word 5722   Oncon0 5723   suc csuc 5725   omcom 7065   ~~ cen 7952   Fincfn 7955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-br 4654  df-opab 4713  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-om 7066  df-1o 7560  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959
This theorem is referenced by:  fin23lem23  9148
  Copyright terms: Public domain W3C validator