Step |
Hyp |
Ref |
Expression |
1 |
|
inf3lem.1 |
|- G = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) |
2 |
|
inf3lem.2 |
|- F = ( rec ( G , (/) ) |` _om ) |
3 |
|
inf3lem.3 |
|- A e. _V |
4 |
|
inf3lem.4 |
|- B e. _V |
5 |
|
fveq2 |
|- ( v = (/) -> ( F ` v ) = ( F ` (/) ) ) |
6 |
5
|
neeq1d |
|- ( v = (/) -> ( ( F ` v ) =/= x <-> ( F ` (/) ) =/= x ) ) |
7 |
6
|
imbi2d |
|- ( v = (/) -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` (/) ) =/= x ) ) ) |
8 |
|
fveq2 |
|- ( v = u -> ( F ` v ) = ( F ` u ) ) |
9 |
8
|
neeq1d |
|- ( v = u -> ( ( F ` v ) =/= x <-> ( F ` u ) =/= x ) ) |
10 |
9
|
imbi2d |
|- ( v = u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` u ) =/= x ) ) ) |
11 |
|
fveq2 |
|- ( v = suc u -> ( F ` v ) = ( F ` suc u ) ) |
12 |
11
|
neeq1d |
|- ( v = suc u -> ( ( F ` v ) =/= x <-> ( F ` suc u ) =/= x ) ) |
13 |
12
|
imbi2d |
|- ( v = suc u -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` suc u ) =/= x ) ) ) |
14 |
|
fveq2 |
|- ( v = A -> ( F ` v ) = ( F ` A ) ) |
15 |
14
|
neeq1d |
|- ( v = A -> ( ( F ` v ) =/= x <-> ( F ` A ) =/= x ) ) |
16 |
15
|
imbi2d |
|- ( v = A -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` v ) =/= x ) <-> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` A ) =/= x ) ) ) |
17 |
1 2 3 4
|
inf3lemb |
|- ( F ` (/) ) = (/) |
18 |
17
|
eqeq1i |
|- ( ( F ` (/) ) = x <-> (/) = x ) |
19 |
|
eqcom |
|- ( (/) = x <-> x = (/) ) |
20 |
18 19
|
sylbb |
|- ( ( F ` (/) ) = x -> x = (/) ) |
21 |
20
|
necon3i |
|- ( x =/= (/) -> ( F ` (/) ) =/= x ) |
22 |
21
|
adantr |
|- ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` (/) ) =/= x ) |
23 |
|
vex |
|- u e. _V |
24 |
1 2 23 4
|
inf3lemd |
|- ( u e. _om -> ( F ` u ) C_ x ) |
25 |
|
df-pss |
|- ( ( F ` u ) C. x <-> ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) ) |
26 |
|
pssnel |
|- ( ( F ` u ) C. x -> E. v ( v e. x /\ -. v e. ( F ` u ) ) ) |
27 |
25 26
|
sylbir |
|- ( ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) -> E. v ( v e. x /\ -. v e. ( F ` u ) ) ) |
28 |
|
ssel |
|- ( x C_ U. x -> ( v e. x -> v e. U. x ) ) |
29 |
|
eluni |
|- ( v e. U. x <-> E. f ( v e. f /\ f e. x ) ) |
30 |
28 29
|
syl6ib |
|- ( x C_ U. x -> ( v e. x -> E. f ( v e. f /\ f e. x ) ) ) |
31 |
|
eleq2 |
|- ( ( F ` suc u ) = x -> ( f e. ( F ` suc u ) <-> f e. x ) ) |
32 |
31
|
biimparc |
|- ( ( f e. x /\ ( F ` suc u ) = x ) -> f e. ( F ` suc u ) ) |
33 |
1 2 23 4
|
inf3lemc |
|- ( u e. _om -> ( F ` suc u ) = ( G ` ( F ` u ) ) ) |
34 |
33
|
eleq2d |
|- ( u e. _om -> ( f e. ( F ` suc u ) <-> f e. ( G ` ( F ` u ) ) ) ) |
35 |
|
elin |
|- ( v e. ( f i^i x ) <-> ( v e. f /\ v e. x ) ) |
36 |
|
vex |
|- f e. _V |
37 |
|
fvex |
|- ( F ` u ) e. _V |
38 |
1 2 36 37
|
inf3lema |
|- ( f e. ( G ` ( F ` u ) ) <-> ( f e. x /\ ( f i^i x ) C_ ( F ` u ) ) ) |
39 |
38
|
simprbi |
|- ( f e. ( G ` ( F ` u ) ) -> ( f i^i x ) C_ ( F ` u ) ) |
40 |
39
|
sseld |
|- ( f e. ( G ` ( F ` u ) ) -> ( v e. ( f i^i x ) -> v e. ( F ` u ) ) ) |
41 |
35 40
|
syl5bir |
|- ( f e. ( G ` ( F ` u ) ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) ) |
42 |
34 41
|
syl6bi |
|- ( u e. _om -> ( f e. ( F ` suc u ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) ) ) |
43 |
32 42
|
syl5 |
|- ( u e. _om -> ( ( f e. x /\ ( F ` suc u ) = x ) -> ( ( v e. f /\ v e. x ) -> v e. ( F ` u ) ) ) ) |
44 |
43
|
com23 |
|- ( u e. _om -> ( ( v e. f /\ v e. x ) -> ( ( f e. x /\ ( F ` suc u ) = x ) -> v e. ( F ` u ) ) ) ) |
45 |
44
|
exp5c |
|- ( u e. _om -> ( v e. f -> ( v e. x -> ( f e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) ) |
46 |
45
|
com34 |
|- ( u e. _om -> ( v e. f -> ( f e. x -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) ) |
47 |
46
|
impd |
|- ( u e. _om -> ( ( v e. f /\ f e. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) |
48 |
47
|
exlimdv |
|- ( u e. _om -> ( E. f ( v e. f /\ f e. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) |
49 |
30 48
|
sylan9r |
|- ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) ) |
50 |
49
|
pm2.43d |
|- ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) ) |
51 |
|
id |
|- ( ( ( F ` suc u ) = x -> v e. ( F ` u ) ) -> ( ( F ` suc u ) = x -> v e. ( F ` u ) ) ) |
52 |
51
|
necon3bd |
|- ( ( ( F ` suc u ) = x -> v e. ( F ` u ) ) -> ( -. v e. ( F ` u ) -> ( F ` suc u ) =/= x ) ) |
53 |
50 52
|
syl6 |
|- ( ( u e. _om /\ x C_ U. x ) -> ( v e. x -> ( -. v e. ( F ` u ) -> ( F ` suc u ) =/= x ) ) ) |
54 |
53
|
impd |
|- ( ( u e. _om /\ x C_ U. x ) -> ( ( v e. x /\ -. v e. ( F ` u ) ) -> ( F ` suc u ) =/= x ) ) |
55 |
54
|
exlimdv |
|- ( ( u e. _om /\ x C_ U. x ) -> ( E. v ( v e. x /\ -. v e. ( F ` u ) ) -> ( F ` suc u ) =/= x ) ) |
56 |
27 55
|
syl5 |
|- ( ( u e. _om /\ x C_ U. x ) -> ( ( ( F ` u ) C_ x /\ ( F ` u ) =/= x ) -> ( F ` suc u ) =/= x ) ) |
57 |
24 56
|
sylani |
|- ( ( u e. _om /\ x C_ U. x ) -> ( ( u e. _om /\ ( F ` u ) =/= x ) -> ( F ` suc u ) =/= x ) ) |
58 |
57
|
exp4b |
|- ( u e. _om -> ( x C_ U. x -> ( u e. _om -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) ) ) |
59 |
58
|
pm2.43a |
|- ( u e. _om -> ( x C_ U. x -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) ) |
60 |
59
|
adantld |
|- ( u e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( ( F ` u ) =/= x -> ( F ` suc u ) =/= x ) ) ) |
61 |
60
|
a2d |
|- ( u e. _om -> ( ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` u ) =/= x ) -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` suc u ) =/= x ) ) ) |
62 |
7 10 13 16 22 61
|
finds |
|- ( A e. _om -> ( ( x =/= (/) /\ x C_ U. x ) -> ( F ` A ) =/= x ) ) |
63 |
62
|
com12 |
|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= x ) ) |