MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin23lem26 Structured version   Visualization version   Unicode version
Theorem fin23lem26 8773
Description: Lemma for fin23lem22 8775. (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 4399 . . . 4 |- ( i = (/) -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ (/) ) )
21rexbidv 2892 . . 3 |- ( i = (/) -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ (/) ) )
3 breq2 4399 . . . 4 |- ( i = a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ a ) )
43rexbidv 2892 . . 3 |- ( i = a -> ( E. j e. S ( j i^i S ) ~~ i <-> E. j e. S ( j i^i S ) ~~ a ) )
5 breq2 4399 . . . 4 |- ( i = suc a -> ( ( j i^i S ) ~~ i <-> ( j i^i S ) ~~ suc a ) )
65rexbidv 2892 . . 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 6720 . . . . . 6 |- Ord om
87a1i 11 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> Ord om )
9 simpl 464 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> S C_ om )
10 0fin 7817 . . . . . . . 8 |- (/) e. Fin
11 eleq1 2537 . . . . . . . 8 |- ( S = (/) -> ( S e. Fin <-> (/) e. Fin ) )
1210, 11mpbiri 241 . . . . . . 7 |- ( S = (/) -> S e. Fin )
1312necon3bi 2669 . . . . . 6 |- ( -. S e. Fin -> S =/= (/) )
1413adantl 473 . . . . 5 |- ( ( S C_ om /\ -. S e. Fin ) -> S =/= (/) )
15 tz7.5 5451 . . . . 5 |- ( ( Ord om /\ S C_ om /\ S =/= (/) ) -> E. j e. S ( S i^i j ) = (/) )
168, 9, 14, 15syl3anc 1292 . . . 4 |- ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( S i^i j ) = (/) )
17 en0 7650 . . . . . 6 |- ( ( j i^i S ) ~~ (/) <-> ( j i^i S ) = (/) )
18 incom 3616 . . . . . . 7 |- ( j i^i S ) = ( S i^i j )
1918eqeq1i 2476 . . . . . 6 |- ( ( j i^i S ) = (/) <-> ( S i^i j ) = (/) )
2017, 19bitri 257 . . . . 5 |- ( ( j i^i S ) ~~ (/) <-> ( S i^i j ) = (/) )
2120rexbii 2881 . . . 4 |- ( E. j e. S ( j i^i S ) ~~ (/) <-> E. j e. S ( S i^i j ) = (/) )
2216, 21sylibr 217 . . 3 |- ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ (/) )
23 simplrl 778 . . . . . . . . . . 11 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ om )
24 omsson 6715 . . . . . . . . . . 11 |- om C_ On
2523, 24syl6ss 3430 . . . . . . . . . 10 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> S C_ On )
2625ssdifssd 3560 . . . . . . . . 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 770 . . . . . . . . . . . 12 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> -. S e. Fin )
28 ssel2 3413 . . . . . . . . . . . . . . 15 |- ( ( S C_ om /\ j e. S ) -> j e. om )
29 onfin2 7782 . . . . . . . . . . . . . . . . 17 |- om = ( On i^i Fin )
30 inss2 3644 . . . . . . . . . . . . . . . . 17 |- ( On i^i Fin ) C_ Fin
3129, 30eqsstri 3448 . . . . . . . . . . . . . . . 16 |- om C_ Fin
32 peano2 6732 . . . . . . . . . . . . . . . 16 |- ( j e. om -> suc j e. om )
3331, 32sseldi 3416 . . . . . . . . . . . . . . 15 |- ( j e. om -> suc j e. Fin )
3428, 33syl 17 . . . . . . . . . . . . . 14 |- ( ( S C_ om /\ j e. S ) -> suc j e. Fin )
3534adantlr 729 . . . . . . . . . . . . 13 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> suc j e. Fin )
36 ssfi 7810 . . . . . . . . . . . . . 14 |- ( ( suc j e. Fin /\ S C_ suc j ) -> S e. Fin )
3736ex 441 . . . . . . . . . . . . 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 182 . . . . . . . . . . 11 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> -. S C_ suc j )
40 ssdif0 3741 . . . . . . . . . . . 12 |- ( S C_ suc j <-> ( S \ suc j ) = (/) )
4140necon3bbii 2690 . . . . . . . . . . 11 |- ( -. S C_ suc j <-> ( S \ suc j ) =/= (/) )
4239, 41sylib 201 . . . . . . . . . 10 |- ( ( ( S C_ om /\ -. S e. Fin ) /\ j e. S ) -> ( S \ suc j ) =/= (/) )
4342ad2ant2lr 762 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( S \ suc j ) =/= (/) )
44 onint 6641 . . . . . . . . 9 |- ( ( ( S \ suc j ) C_ On /\ ( S \ suc j ) =/= (/) ) -> |^| ( S \ suc j ) e. ( S \ suc j ) )
4526, 43, 44syl2anc 673 . . . . . . . 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 3402 . . . . . . 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 774 . . . . . . . . 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 3034 . . . . . . . . . . 11 |- j e. _V
49 vex 3034 . . . . . . . . . . 11 |- a e. _V
50 en2sn 7667 . . . . . . . . . . 11 |- ( ( j e. _V /\ a e. _V ) -> { j } ~~ { a } )
5148, 49, 50mp2an 686 . . . . . . . . . 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 772 . . . . . . . . . . . 12 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. S )
5423, 53sseldd 3419 . . . . . . . . . . 11 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> j e. om )
55 nnord 6719 . . . . . . . . . . 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 5448 . . . . . . . . . . . 12 |- ( Ord j -> -. j e. j )
58 inss1 3643 . . . . . . . . . . . . 13 |- ( j i^i S ) C_ j
5958sseli 3414 . . . . . . . . . . . 12 |- ( j e. ( j i^i S ) -> j e. j )
6057, 59nsyl 125 . . . . . . . . . . 11 |- ( Ord j -> -. j e. ( j i^i S ) )
61 disjsn 4023 . . . . . . . . . . 11 |- ( ( ( j i^i S ) i^i { j } ) = (/) <-> -. j e. ( j i^i S ) )
6260, 61sylibr 217 . . . . . . . . . 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 6719 . . . . . . . . . . . 12 |- ( a e. om -> Ord a )
65 ordirr 5448 . . . . . . . . . . . 12 |- ( Ord a -> -. a e. a )
6664, 65syl 17 . . . . . . . . . . 11 |- ( a e. om -> -. a e. a )
67 disjsn 4023 . . . . . . . . . . 11 |- ( ( a i^i { a } ) = (/) <-> -. a e. a )
6866, 67sylibr 217 . . . . . . . . . 10 |- ( a e. om -> ( a i^i { a } ) = (/) )
6968ad2antrr 740 . . . . . . . . 9 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> ( a i^i { a } ) = (/) )
70 unen 7670 . . . . . . . . 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 1293 . . . . . . . 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 774 . . . . . . . . . . . . . . . 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 778 . . . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . 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 6660 . . . . . . . . . . . . . . . . . 18 |- ( Ord j <-> Ord suc j )
7656, 75sylib 201 . . . . . . . . . . . . . . . . 17 |- ( ( ( a e. om /\ ( S C_ om /\ -. S e. Fin ) ) /\ ( j e. S /\ ( j i^i S ) ~~ a ) ) -> Ord suc j )
7776adantrr 731 . . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> S C_ On )
7978ssdifssd 3560 . . . . . . . . . . . . . . . . . . . 20 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( S \ suc j ) C_ On )
80 simpl1 1033 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. S )
81 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> -. b e. suc j )
8280, 81eldifd 3401 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ -. b e. suc j ) -> b e. ( S \ suc j ) )
8382ex 441 . . . . . . . . . . . . . . . . . . . 20 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> b e. ( S \ suc j ) ) )
84 onnmin 6649 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( S \ suc j ) C_ On /\ b e. ( S \ suc j ) ) -> -. b e. |^| ( S \ suc j ) )
8579, 83, 84syl6an 554 . . . . . . . . . . . . . . . . . . 19 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( -. b e. suc j -> -. b e. |^| ( S \ suc j ) ) )
8685con4d 108 . . . . . . . . . . . . . . . . . 18 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) -> b e. suc j ) )
8786imp 436 . . . . . . . . . . . . . . . . 17 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. |^| ( S \ suc j ) ) -> b e. suc j )
88 simp3 1032 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> Ord suc j )
89 ordsucss 6664 . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> suc b C_ suc j )
9291sscond 3559 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> ( S \ suc j ) C_ ( S \ suc b ) )
93 intss 4247 . . . . . . . . . . . . . . . . . . 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 1034 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> S C_ On )
96 ordelon 5454 . . . . . . . . . . . . . . . . . . . 20 |- ( ( Ord suc j /\ b e. suc j ) -> b e. On )
9788, 96sylan 479 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. On )
98 onmindif 5519 . . . . . . . . . . . . . . . . . . 19 |- ( ( S C_ On /\ b e. On ) -> b e. |^| ( S \ suc b ) )
9995, 97, 98syl2anc 673 . . . . . . . . . . . . . . . . . 18 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc b ) )
10094, 99sseldd 3419 . . . . . . . . . . . . . . . . 17 |- ( ( ( b e. S /\ S C_ On /\ Ord suc j ) /\ b e. suc j ) -> b e. |^| ( S \ suc j ) )
10187, 100impbida 850 . . . . . . . . . . . . . . . 16 |- ( ( b e. S /\ S C_ On /\ Ord suc j ) -> ( b e. |^| ( S \ suc j ) <-> b e. suc j ) )
10272, 74, 77, 101syl3anc 1292 . . . . . . . . . . . . . . 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 5436 . . . . . . . . . . . . . . . 16 |- suc j = ( j u. { j } )
104103eleq2i 2541 . . . . . . . . . . . . . . 15 |- ( b e. suc j <-> b e. ( j u. { j } ) )
105102, 104syl6bb 269 . . . . . . . . . . . . . 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 626 . . . . . . . . . . . . 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 652 . . . . . . . . . . . 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 3608 . . . . . . . . . . . 12 |- ( b e. ( |^| ( S \ suc j ) i^i S ) <-> ( b e. |^| ( S \ suc j ) /\ b e. S ) )
109 elin 3608 . . . . . . . . . . . 12 |- ( b e. ( ( j u. { j } ) i^i S ) <-> ( b e. ( j u. { j } ) /\ b e. S ) )
110107, 108, 1093bitr4g 296 . . . . . . . . . . 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 2469 . . . . . . . . . 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 3682 . . . . . . . . . 10 |- ( ( j u. { j } ) i^i S ) = ( ( j i^i S ) u. ( { j } i^i S ) )
113111, 112syl6eq 2521 . . . . . . . . 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 4107 . . . . . . . . . . . 12 |- ( j e. S -> { j } C_ S )
115 df-ss 3404 . . . . . . . . . . . 12 |- ( { j } C_ S <-> ( { j } i^i S ) = { j } )
116114, 115sylib 201 . . . . . . . . . . 11 |- ( j e. S -> ( { j } i^i S ) = { j } )
117116uneq2d 3579 . . . . . . . . . 10 |- ( j e. S -> ( ( j i^i S ) u. ( { j } i^i S ) ) = ( ( j i^i S ) u. { j } ) )
118117ad2antrl 742 . . . . . . . . 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 2505 . . . . . . . 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 5436 . . . . . . . . 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 4426 . . . . . . 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 3618 . . . . . . . . 9 |- ( b = |^| ( S \ suc j ) -> ( b i^i S ) = ( |^| ( S \ suc j ) i^i S ) )
124123breq1d 4405 . . . . . . . 8 |- ( b = |^| ( S \ suc j ) -> ( ( b i^i S ) ~~ suc a <-> ( |^| ( S \ suc j ) i^i S ) ~~ suc a ) )
125124rspcev 3136 . . . . . . 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 673 . . . . . 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 2872 . . . . 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 3618 . . . . . . 7 |- ( b = j -> ( b i^i S ) = ( j i^i S ) )
129128breq1d 4405 . . . . . 6 |- ( b = j -> ( ( b i^i S ) ~~ suc a <-> ( j i^i S ) ~~ suc a ) )
130129cbvrexv 3006 . . . . 5 |- ( E. b e. S ( b i^i S ) ~~ suc a <-> E. j e. S ( j i^i S ) ~~ suc a )
131127, 130syl6ib 234 . . . 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 441 . . 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 6740 . 2 |- ( i e. om -> ( ( S C_ om /\ -. S e. Fin ) -> E. j e. S ( j i^i S ) ~~ i ) )
134133impcom 437 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 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   E.wrex 2757   _Vcvv 3031   \ cdif 3387   u. cun 3388   i^i cin 3389   C_ wss 3390   (/)c0 3722   {csn 3959   |^|cint 4226   class class class wbr 4395   Ord word 5429   Oncon0 5430   suc csuc 5432   omcom 6711   ~~ cen 7584   Fincfn 7587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-br 4396  df-opab 4455  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-om 6712  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591
This theorem is referenced by:  fin23lem23  8774
  Copyright terms: Public domain W3C validator