Step | Hyp | Ref
| Expression |
1 | | sspr 4746 |
. . . . 5
⊢ (𝑥 ⊆ {∅, 𝐴} ↔ ((𝑥 = ∅ ∨ 𝑥 = {∅}) ∨ (𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴}))) |
2 | | unieq 4830 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) |
3 | | uni0 4849 |
. . . . . . . . . 10
⊢ ∪ ∅ = ∅ |
4 | | 0ex 5200 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
5 | 4 | prid1 4678 |
. . . . . . . . . 10
⊢ ∅
∈ {∅, 𝐴} |
6 | 3, 5 | eqeltri 2834 |
. . . . . . . . 9
⊢ ∪ ∅ ∈ {∅, 𝐴} |
7 | 2, 6 | eqeltrdi 2846 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ∪ 𝑥
∈ {∅, 𝐴}) |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 = ∅ → ∪ 𝑥
∈ {∅, 𝐴})) |
9 | | unieq 4830 |
. . . . . . . . 9
⊢ (𝑥 = {∅} → ∪ 𝑥 =
∪ {∅}) |
10 | 4 | unisn 4841 |
. . . . . . . . . 10
⊢ ∪ {∅} = ∅ |
11 | 10, 5 | eqeltri 2834 |
. . . . . . . . 9
⊢ ∪ {∅} ∈ {∅, 𝐴} |
12 | 9, 11 | eqeltrdi 2846 |
. . . . . . . 8
⊢ (𝑥 = {∅} → ∪ 𝑥
∈ {∅, 𝐴}) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 = {∅} → ∪ 𝑥
∈ {∅, 𝐴})) |
14 | 8, 13 | jaod 859 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = ∅ ∨ 𝑥 = {∅}) → ∪ 𝑥
∈ {∅, 𝐴})) |
15 | | unieq 4830 |
. . . . . . . . . 10
⊢ (𝑥 = {𝐴} → ∪ 𝑥 = ∪
{𝐴}) |
16 | | unisng 4840 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
17 | 15, 16 | sylan9eqr 2800 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {𝐴}) → ∪ 𝑥 = 𝐴) |
18 | | prid2g 4677 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {∅, 𝐴}) |
19 | 18 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {∅, 𝐴}) |
20 | 17, 19 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {𝐴}) → ∪ 𝑥 ∈ {∅, 𝐴}) |
21 | 20 | ex 416 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 = {𝐴} → ∪ 𝑥 ∈ {∅, 𝐴})) |
22 | | unieq 4830 |
. . . . . . . . . 10
⊢ (𝑥 = {∅, 𝐴} → ∪ 𝑥 = ∪
{∅, 𝐴}) |
23 | | uniprg 4836 |
. . . . . . . . . . . 12
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ∪ {∅, 𝐴} = (∅ ∪ 𝐴)) |
24 | 4, 23 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ∪
{∅, 𝐴} = (∅
∪ 𝐴)) |
25 | | uncom 4067 |
. . . . . . . . . . . 12
⊢ (∅
∪ 𝐴) = (𝐴 ∪ ∅) |
26 | | un0 4305 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ ∅) = 𝐴 |
27 | 25, 26 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (∅
∪ 𝐴) = 𝐴 |
28 | 24, 27 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ∪
{∅, 𝐴} = 𝐴) |
29 | 22, 28 | sylan9eqr 2800 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {∅, 𝐴}) → ∪ 𝑥 = 𝐴) |
30 | 18 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {∅, 𝐴}) → 𝐴 ∈ {∅, 𝐴}) |
31 | 29, 30 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = {∅, 𝐴}) → ∪ 𝑥 ∈ {∅, 𝐴}) |
32 | 31 | ex 416 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 = {∅, 𝐴} → ∪ 𝑥 ∈ {∅, 𝐴})) |
33 | 21, 32 | jaod 859 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴}) → ∪ 𝑥 ∈ {∅, 𝐴})) |
34 | 14, 33 | jaod 859 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (((𝑥 = ∅ ∨ 𝑥 = {∅}) ∨ (𝑥 = {𝐴} ∨ 𝑥 = {∅, 𝐴})) → ∪
𝑥 ∈ {∅, 𝐴})) |
35 | 1, 34 | syl5bi 245 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ {∅, 𝐴} → ∪ 𝑥 ∈ {∅, 𝐴})) |
36 | 35 | alrimiv 1935 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ {∅, 𝐴} → ∪ 𝑥 ∈ {∅, 𝐴})) |
37 | | vex 3412 |
. . . . . 6
⊢ 𝑥 ∈ V |
38 | 37 | elpr 4564 |
. . . . 5
⊢ (𝑥 ∈ {∅, 𝐴} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) |
39 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
40 | 39 | elpr 4564 |
. . . . . . . 8
⊢ (𝑦 ∈ {∅, 𝐴} ↔ (𝑦 = ∅ ∨ 𝑦 = 𝐴)) |
41 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → 𝑦 = ∅) |
42 | 41 | ineq2d 4127 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) = (𝑥 ∩ ∅)) |
43 | | in0 4306 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∩ ∅) =
∅ |
44 | 42, 43 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) = ∅) |
45 | 44, 5 | eqeltrdi 2846 |
. . . . . . . . . . 11
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = ∅ ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
47 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = ∅) → 𝑦 = ∅) |
48 | 47 | ineq2d 4127 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) = (𝑥 ∩ ∅)) |
49 | 48, 43 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) = ∅) |
50 | 49, 5 | eqeltrdi 2846 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = 𝐴 ∧ 𝑦 = ∅) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
52 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → 𝑥 = ∅) |
53 | 52 | ineq1d 4126 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) = (∅ ∩ 𝑦)) |
54 | | 0in 4308 |
. . . . . . . . . . . . 13
⊢ (∅
∩ 𝑦) =
∅ |
55 | 53, 54 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) = ∅) |
56 | 55, 5 | eqeltrdi 2846 |
. . . . . . . . . . 11
⊢ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = ∅ ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
58 | | ineq12 4122 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝐴)) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝐴)) |
60 | | inidm 4133 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
61 | 59, 60 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) → (𝑥 ∩ 𝑦) = 𝐴) |
62 | 18 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) → 𝐴 ∈ {∅, 𝐴}) |
63 | 61, 62 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
64 | 63 | ex 416 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
65 | 46, 51, 57, 64 | ccased 1039 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (((𝑥 = ∅ ∨ 𝑥 = 𝐴) ∧ (𝑦 = ∅ ∨ 𝑦 = 𝐴)) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
66 | 65 | expdimp 456 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → ((𝑦 = ∅ ∨ 𝑦 = 𝐴) → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
67 | 40, 66 | syl5bi 245 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → (𝑦 ∈ {∅, 𝐴} → (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
68 | 67 | ralrimiv 3104 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) → ∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
69 | 68 | ex 416 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) → ∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
70 | 38, 69 | syl5bi 245 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ {∅, 𝐴} → ∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴})) |
71 | 70 | ralrimiv 3104 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}) |
72 | | prex 5325 |
. . . 4
⊢ {∅,
𝐴} ∈
V |
73 | | istopg 21792 |
. . . 4
⊢
({∅, 𝐴} ∈
V → ({∅, 𝐴}
∈ Top ↔ (∀𝑥(𝑥 ⊆ {∅, 𝐴} → ∪ 𝑥 ∈ {∅, 𝐴}) ∧ ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}))) |
74 | 72, 73 | mp1i 13 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ({∅, 𝐴} ∈ Top ↔ (∀𝑥(𝑥 ⊆ {∅, 𝐴} → ∪ 𝑥 ∈ {∅, 𝐴}) ∧ ∀𝑥 ∈ {∅, 𝐴}∀𝑦 ∈ {∅, 𝐴} (𝑥 ∩ 𝑦) ∈ {∅, 𝐴}))) |
75 | 36, 71, 74 | mpbir2and 713 |
. 2
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ Top) |
76 | 28 | eqcomd 2743 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 = ∪ {∅,
𝐴}) |
77 | | istopon 21809 |
. 2
⊢
({∅, 𝐴} ∈
(TopOn‘𝐴) ↔
({∅, 𝐴} ∈ Top
∧ 𝐴 = ∪ {∅, 𝐴})) |
78 | 75, 76, 77 | sylanbrc 586 |
1
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) |