Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
|- ( A =/= (/) <-> E. z z e. A ) |
2 |
|
snssi |
|- ( z e. A -> { z } C_ A ) |
3 |
2
|
anim2i |
|- ( ( { z } C_ y /\ z e. A ) -> ( { z } C_ y /\ { z } C_ A ) ) |
4 |
|
ssin |
|- ( ( { z } C_ y /\ { z } C_ A ) <-> { z } C_ ( y i^i A ) ) |
5 |
|
vex |
|- z e. _V |
6 |
5
|
snss |
|- ( z e. ( y i^i A ) <-> { z } C_ ( y i^i A ) ) |
7 |
4 6
|
bitr4i |
|- ( ( { z } C_ y /\ { z } C_ A ) <-> z e. ( y i^i A ) ) |
8 |
3 7
|
sylib |
|- ( ( { z } C_ y /\ z e. A ) -> z e. ( y i^i A ) ) |
9 |
8
|
ne0d |
|- ( ( { z } C_ y /\ z e. A ) -> ( y i^i A ) =/= (/) ) |
10 |
|
inss2 |
|- ( y i^i A ) C_ A |
11 |
|
vex |
|- y e. _V |
12 |
11
|
inex1 |
|- ( y i^i A ) e. _V |
13 |
12
|
epfrc |
|- ( ( _E Fr A /\ ( y i^i A ) C_ A /\ ( y i^i A ) =/= (/) ) -> E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) ) |
14 |
10 13
|
mp3an2 |
|- ( ( _E Fr A /\ ( y i^i A ) =/= (/) ) -> E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) ) |
15 |
|
elin |
|- ( x e. ( y i^i A ) <-> ( x e. y /\ x e. A ) ) |
16 |
15
|
anbi1i |
|- ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( ( x e. y /\ x e. A ) /\ ( ( y i^i A ) i^i x ) = (/) ) ) |
17 |
|
anass |
|- ( ( ( x e. y /\ x e. A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) ) |
18 |
16 17
|
bitri |
|- ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) ) |
19 |
|
n0 |
|- ( ( x i^i A ) =/= (/) <-> E. w w e. ( x i^i A ) ) |
20 |
|
elinel1 |
|- ( w e. ( x i^i A ) -> w e. x ) |
21 |
20
|
ancri |
|- ( w e. ( x i^i A ) -> ( w e. x /\ w e. ( x i^i A ) ) ) |
22 |
|
trel |
|- ( Tr y -> ( ( w e. x /\ x e. y ) -> w e. y ) ) |
23 |
|
inass |
|- ( ( y i^i A ) i^i x ) = ( y i^i ( A i^i x ) ) |
24 |
|
incom |
|- ( A i^i x ) = ( x i^i A ) |
25 |
24
|
ineq2i |
|- ( y i^i ( A i^i x ) ) = ( y i^i ( x i^i A ) ) |
26 |
23 25
|
eqtri |
|- ( ( y i^i A ) i^i x ) = ( y i^i ( x i^i A ) ) |
27 |
26
|
eleq2i |
|- ( w e. ( ( y i^i A ) i^i x ) <-> w e. ( y i^i ( x i^i A ) ) ) |
28 |
|
elin |
|- ( w e. ( y i^i ( x i^i A ) ) <-> ( w e. y /\ w e. ( x i^i A ) ) ) |
29 |
27 28
|
bitr2i |
|- ( ( w e. y /\ w e. ( x i^i A ) ) <-> w e. ( ( y i^i A ) i^i x ) ) |
30 |
|
ne0i |
|- ( w e. ( ( y i^i A ) i^i x ) -> ( ( y i^i A ) i^i x ) =/= (/) ) |
31 |
29 30
|
sylbi |
|- ( ( w e. y /\ w e. ( x i^i A ) ) -> ( ( y i^i A ) i^i x ) =/= (/) ) |
32 |
31
|
ex |
|- ( w e. y -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) |
33 |
22 32
|
syl6 |
|- ( Tr y -> ( ( w e. x /\ x e. y ) -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
34 |
33
|
expd |
|- ( Tr y -> ( w e. x -> ( x e. y -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) ) |
35 |
34
|
com34 |
|- ( Tr y -> ( w e. x -> ( w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) ) |
36 |
35
|
impd |
|- ( Tr y -> ( ( w e. x /\ w e. ( x i^i A ) ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
37 |
21 36
|
syl5 |
|- ( Tr y -> ( w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
38 |
37
|
exlimdv |
|- ( Tr y -> ( E. w w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
39 |
19 38
|
syl5bi |
|- ( Tr y -> ( ( x i^i A ) =/= (/) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
40 |
39
|
com23 |
|- ( Tr y -> ( x e. y -> ( ( x i^i A ) =/= (/) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) |
41 |
40
|
imp |
|- ( ( Tr y /\ x e. y ) -> ( ( x i^i A ) =/= (/) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) |
42 |
41
|
necon4d |
|- ( ( Tr y /\ x e. y ) -> ( ( ( y i^i A ) i^i x ) = (/) -> ( x i^i A ) = (/) ) ) |
43 |
42
|
anim2d |
|- ( ( Tr y /\ x e. y ) -> ( ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) ) |
44 |
43
|
expimpd |
|- ( Tr y -> ( ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) ) |
45 |
18 44
|
syl5bi |
|- ( Tr y -> ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) ) |
46 |
45
|
reximdv2 |
|- ( Tr y -> ( E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) -> E. x e. A ( x i^i A ) = (/) ) ) |
47 |
14 46
|
syl5 |
|- ( Tr y -> ( ( _E Fr A /\ ( y i^i A ) =/= (/) ) -> E. x e. A ( x i^i A ) = (/) ) ) |
48 |
47
|
expcomd |
|- ( Tr y -> ( ( y i^i A ) =/= (/) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) |
49 |
9 48
|
syl5 |
|- ( Tr y -> ( ( { z } C_ y /\ z e. A ) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) |
50 |
49
|
expd |
|- ( Tr y -> ( { z } C_ y -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) ) |
51 |
50
|
impcom |
|- ( ( { z } C_ y /\ Tr y ) -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) |
52 |
51
|
3adant3 |
|- ( ( { z } C_ y /\ Tr y /\ A. w ( ( { z } C_ w /\ Tr w ) -> y C_ w ) ) -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) |
53 |
|
snex |
|- { z } e. _V |
54 |
53
|
tz9.1 |
|- E. y ( { z } C_ y /\ Tr y /\ A. w ( ( { z } C_ w /\ Tr w ) -> y C_ w ) ) |
55 |
52 54
|
exlimiiv |
|- ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) |
56 |
55
|
exlimiv |
|- ( E. z z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) |
57 |
1 56
|
sylbi |
|- ( A =/= (/) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) |
58 |
57
|
impcom |
|- ( ( _E Fr A /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) ) |