Step |
Hyp |
Ref |
Expression |
1 |
|
sspr |
|- ( x C_ { (/) , A } <-> ( ( x = (/) \/ x = { (/) } ) \/ ( x = { A } \/ x = { (/) , A } ) ) ) |
2 |
|
unieq |
|- ( x = (/) -> U. x = U. (/) ) |
3 |
|
uni0 |
|- U. (/) = (/) |
4 |
|
0ex |
|- (/) e. _V |
5 |
4
|
prid1 |
|- (/) e. { (/) , A } |
6 |
3 5
|
eqeltri |
|- U. (/) e. { (/) , A } |
7 |
2 6
|
eqeltrdi |
|- ( x = (/) -> U. x e. { (/) , A } ) |
8 |
7
|
a1i |
|- ( A e. V -> ( x = (/) -> U. x e. { (/) , A } ) ) |
9 |
|
unieq |
|- ( x = { (/) } -> U. x = U. { (/) } ) |
10 |
4
|
unisn |
|- U. { (/) } = (/) |
11 |
10 5
|
eqeltri |
|- U. { (/) } e. { (/) , A } |
12 |
9 11
|
eqeltrdi |
|- ( x = { (/) } -> U. x e. { (/) , A } ) |
13 |
12
|
a1i |
|- ( A e. V -> ( x = { (/) } -> U. x e. { (/) , A } ) ) |
14 |
8 13
|
jaod |
|- ( A e. V -> ( ( x = (/) \/ x = { (/) } ) -> U. x e. { (/) , A } ) ) |
15 |
|
unieq |
|- ( x = { A } -> U. x = U. { A } ) |
16 |
|
unisng |
|- ( A e. V -> U. { A } = A ) |
17 |
15 16
|
sylan9eqr |
|- ( ( A e. V /\ x = { A } ) -> U. x = A ) |
18 |
|
prid2g |
|- ( A e. V -> A e. { (/) , A } ) |
19 |
18
|
adantr |
|- ( ( A e. V /\ x = { A } ) -> A e. { (/) , A } ) |
20 |
17 19
|
eqeltrd |
|- ( ( A e. V /\ x = { A } ) -> U. x e. { (/) , A } ) |
21 |
20
|
ex |
|- ( A e. V -> ( x = { A } -> U. x e. { (/) , A } ) ) |
22 |
|
unieq |
|- ( x = { (/) , A } -> U. x = U. { (/) , A } ) |
23 |
|
uniprg |
|- ( ( (/) e. _V /\ A e. V ) -> U. { (/) , A } = ( (/) u. A ) ) |
24 |
4 23
|
mpan |
|- ( A e. V -> U. { (/) , A } = ( (/) u. A ) ) |
25 |
|
uncom |
|- ( (/) u. A ) = ( A u. (/) ) |
26 |
|
un0 |
|- ( A u. (/) ) = A |
27 |
25 26
|
eqtri |
|- ( (/) u. A ) = A |
28 |
24 27
|
eqtrdi |
|- ( A e. V -> U. { (/) , A } = A ) |
29 |
22 28
|
sylan9eqr |
|- ( ( A e. V /\ x = { (/) , A } ) -> U. x = A ) |
30 |
18
|
adantr |
|- ( ( A e. V /\ x = { (/) , A } ) -> A e. { (/) , A } ) |
31 |
29 30
|
eqeltrd |
|- ( ( A e. V /\ x = { (/) , A } ) -> U. x e. { (/) , A } ) |
32 |
31
|
ex |
|- ( A e. V -> ( x = { (/) , A } -> U. x e. { (/) , A } ) ) |
33 |
21 32
|
jaod |
|- ( A e. V -> ( ( x = { A } \/ x = { (/) , A } ) -> U. x e. { (/) , A } ) ) |
34 |
14 33
|
jaod |
|- ( A e. V -> ( ( ( x = (/) \/ x = { (/) } ) \/ ( x = { A } \/ x = { (/) , A } ) ) -> U. x e. { (/) , A } ) ) |
35 |
1 34
|
syl5bi |
|- ( A e. V -> ( x C_ { (/) , A } -> U. x e. { (/) , A } ) ) |
36 |
35
|
alrimiv |
|- ( A e. V -> A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) ) |
37 |
|
vex |
|- x e. _V |
38 |
37
|
elpr |
|- ( x e. { (/) , A } <-> ( x = (/) \/ x = A ) ) |
39 |
|
vex |
|- y e. _V |
40 |
39
|
elpr |
|- ( y e. { (/) , A } <-> ( y = (/) \/ y = A ) ) |
41 |
|
simpr |
|- ( ( x = (/) /\ y = (/) ) -> y = (/) ) |
42 |
41
|
ineq2d |
|- ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) = ( x i^i (/) ) ) |
43 |
|
in0 |
|- ( x i^i (/) ) = (/) |
44 |
42 43
|
eqtrdi |
|- ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) = (/) ) |
45 |
44 5
|
eqeltrdi |
|- ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) |
46 |
45
|
a1i |
|- ( A e. V -> ( ( x = (/) /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) ) |
47 |
|
simpr |
|- ( ( x = A /\ y = (/) ) -> y = (/) ) |
48 |
47
|
ineq2d |
|- ( ( x = A /\ y = (/) ) -> ( x i^i y ) = ( x i^i (/) ) ) |
49 |
48 43
|
eqtrdi |
|- ( ( x = A /\ y = (/) ) -> ( x i^i y ) = (/) ) |
50 |
49 5
|
eqeltrdi |
|- ( ( x = A /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) |
51 |
50
|
a1i |
|- ( A e. V -> ( ( x = A /\ y = (/) ) -> ( x i^i y ) e. { (/) , A } ) ) |
52 |
|
simpl |
|- ( ( x = (/) /\ y = A ) -> x = (/) ) |
53 |
52
|
ineq1d |
|- ( ( x = (/) /\ y = A ) -> ( x i^i y ) = ( (/) i^i y ) ) |
54 |
|
0in |
|- ( (/) i^i y ) = (/) |
55 |
53 54
|
eqtrdi |
|- ( ( x = (/) /\ y = A ) -> ( x i^i y ) = (/) ) |
56 |
55 5
|
eqeltrdi |
|- ( ( x = (/) /\ y = A ) -> ( x i^i y ) e. { (/) , A } ) |
57 |
56
|
a1i |
|- ( A e. V -> ( ( x = (/) /\ y = A ) -> ( x i^i y ) e. { (/) , A } ) ) |
58 |
|
ineq12 |
|- ( ( x = A /\ y = A ) -> ( x i^i y ) = ( A i^i A ) ) |
59 |
58
|
adantl |
|- ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) = ( A i^i A ) ) |
60 |
|
inidm |
|- ( A i^i A ) = A |
61 |
59 60
|
eqtrdi |
|- ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) = A ) |
62 |
18
|
adantr |
|- ( ( A e. V /\ ( x = A /\ y = A ) ) -> A e. { (/) , A } ) |
63 |
61 62
|
eqeltrd |
|- ( ( A e. V /\ ( x = A /\ y = A ) ) -> ( x i^i y ) e. { (/) , A } ) |
64 |
63
|
ex |
|- ( A e. V -> ( ( x = A /\ y = A ) -> ( x i^i y ) e. { (/) , A } ) ) |
65 |
46 51 57 64
|
ccased |
|- ( A e. V -> ( ( ( x = (/) \/ x = A ) /\ ( y = (/) \/ y = A ) ) -> ( x i^i y ) e. { (/) , A } ) ) |
66 |
65
|
expdimp |
|- ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> ( ( y = (/) \/ y = A ) -> ( x i^i y ) e. { (/) , A } ) ) |
67 |
40 66
|
syl5bi |
|- ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> ( y e. { (/) , A } -> ( x i^i y ) e. { (/) , A } ) ) |
68 |
67
|
ralrimiv |
|- ( ( A e. V /\ ( x = (/) \/ x = A ) ) -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) |
69 |
68
|
ex |
|- ( A e. V -> ( ( x = (/) \/ x = A ) -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) |
70 |
38 69
|
syl5bi |
|- ( A e. V -> ( x e. { (/) , A } -> A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) |
71 |
70
|
ralrimiv |
|- ( A e. V -> A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) |
72 |
|
prex |
|- { (/) , A } e. _V |
73 |
|
istopg |
|- ( { (/) , A } e. _V -> ( { (/) , A } e. Top <-> ( A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) /\ A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) ) |
74 |
72 73
|
mp1i |
|- ( A e. V -> ( { (/) , A } e. Top <-> ( A. x ( x C_ { (/) , A } -> U. x e. { (/) , A } ) /\ A. x e. { (/) , A } A. y e. { (/) , A } ( x i^i y ) e. { (/) , A } ) ) ) |
75 |
36 71 74
|
mpbir2and |
|- ( A e. V -> { (/) , A } e. Top ) |
76 |
28
|
eqcomd |
|- ( A e. V -> A = U. { (/) , A } ) |
77 |
|
istopon |
|- ( { (/) , A } e. ( TopOn ` A ) <-> ( { (/) , A } e. Top /\ A = U. { (/) , A } ) ) |
78 |
75 76 77
|
sylanbrc |
|- ( A e. V -> { (/) , A } e. ( TopOn ` A ) ) |