Step | Hyp | Ref
| Expression |
1 | | hausdiag.x |
. . 3
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | ishaus 20936 |
. 2
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
3 | | txtop 21182 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
4 | 3 | anidms 675 |
. . . . 5
⊢ (𝐽 ∈ Top → (𝐽 ×t 𝐽) ∈ Top) |
5 | | f1oi 6086 |
. . . . . . 7
⊢ ( I
↾ 𝑋):𝑋–1-1-onto→𝑋 |
6 | | f1of 6050 |
. . . . . . 7
⊢ (( I
↾ 𝑋):𝑋–1-1-onto→𝑋 → ( I ↾ 𝑋):𝑋⟶𝑋) |
7 | | fssxp 5973 |
. . . . . . 7
⊢ (( I
↾ 𝑋):𝑋⟶𝑋 → ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . 6
⊢ ( I
↾ 𝑋) ⊆ (𝑋 × 𝑋) |
9 | 1, 1 | txuni 21205 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
10 | 9 | anidms 675 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
11 | 8, 10 | syl5sseq 3616 |
. . . . 5
⊢ (𝐽 ∈ Top → ( I ↾
𝑋) ⊆ ∪ (𝐽
×t 𝐽)) |
12 | | eqid 2610 |
. . . . . 6
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
13 | 12 | iscld2 20642 |
. . . . 5
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ( I ↾
𝑋) ⊆ ∪ (𝐽
×t 𝐽))
→ (( I ↾ 𝑋)
∈ (Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×t 𝐽))) |
14 | 4, 11, 13 | syl2anc 691 |
. . . 4
⊢ (𝐽 ∈ Top → (( I ↾
𝑋) ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×t 𝐽))) |
15 | | eltx 21181 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
∈ (𝐽
×t 𝐽)
↔ ∀𝑒 ∈
(∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
16 | 15 | anidms 675 |
. . . 4
⊢ (𝐽 ∈ Top → ((∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
∈ (𝐽
×t 𝐽)
↔ ∀𝑒 ∈
(∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
17 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
↔ (𝑒 ∈ ∪ (𝐽
×t 𝐽)
∧ ¬ 𝑒 ∈ ( I
↾ 𝑋))) |
18 | 10 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top → ∪ (𝐽
×t 𝐽) =
(𝑋 × 𝑋)) |
19 | 18 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽
×t 𝐽)
↔ 𝑒 ∈ (𝑋 × 𝑋))) |
20 | 19 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽
×t 𝐽)
∧ ¬ 𝑒 ∈ ( I
↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))) |
21 | 17, 20 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))) |
22 | 21 | imbi1d 330 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
→ ∃𝑐 ∈
𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
23 | | impexp 461 |
. . . . . . . 8
⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
24 | 22, 23 | syl6bb 275 |
. . . . . . 7
⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
→ ∃𝑐 ∈
𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))))) |
25 | 24 | ralbidv2 2967 |
. . . . . 6
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
26 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑒 = 〈𝑎, 𝑏〉 → (𝑒 ∈ ( I ↾ 𝑋) ↔ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋))) |
27 | 26 | notbid 307 |
. . . . . . . 8
⊢ (𝑒 = 〈𝑎, 𝑏〉 → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋))) |
28 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑒 = 〈𝑎, 𝑏〉 → (𝑒 ∈ (𝑐 × 𝑑) ↔ 〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑))) |
29 | 28 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑒 = 〈𝑎, 𝑏〉 → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
30 | 29 | 2rexbidv 3039 |
. . . . . . . 8
⊢ (𝑒 = 〈𝑎, 𝑏〉 → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
31 | 27, 30 | imbi12d 333 |
. . . . . . 7
⊢ (𝑒 = 〈𝑎, 𝑏〉 → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (¬
〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
32 | 31 | ralxp 5185 |
. . . . . 6
⊢
(∀𝑒 ∈
(𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
33 | 25, 32 | syl6bb 275 |
. . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
34 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
35 | 34 | opelres 5322 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) ↔ (〈𝑎, 𝑏〉 ∈ I ∧ 𝑎 ∈ 𝑋)) |
36 | | df-br 4584 |
. . . . . . . . . . . 12
⊢ (𝑎 I 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ I ) |
37 | 34 | ideq 5196 |
. . . . . . . . . . . 12
⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏) |
38 | 36, 37 | bitr3i 265 |
. . . . . . . . . . 11
⊢
(〈𝑎, 𝑏〉 ∈ I ↔ 𝑎 = 𝑏) |
39 | | iba 523 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑋 → (〈𝑎, 𝑏〉 ∈ I ↔ (〈𝑎, 𝑏〉 ∈ I ∧ 𝑎 ∈ 𝑋))) |
40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (〈𝑎, 𝑏〉 ∈ I ↔ (〈𝑎, 𝑏〉 ∈ I ∧ 𝑎 ∈ 𝑋))) |
41 | 38, 40 | syl5rbbr 274 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((〈𝑎, 𝑏〉 ∈ I ∧ 𝑎 ∈ 𝑋) ↔ 𝑎 = 𝑏)) |
42 | 35, 41 | syl5bb 271 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏)) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏)) |
44 | 43 | necon3bbid 2819 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏)) |
45 | | elssuni 4403 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽) |
46 | | elssuni 4403 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽) |
47 | | xpss12 5148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ⊆ ∪ 𝐽
∧ 𝑑 ⊆ ∪ 𝐽)
→ (𝑐 × 𝑑) ⊆ (∪ 𝐽
× ∪ 𝐽)) |
48 | 45, 46, 47 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽)) |
49 | 1, 1 | xpeq12i 5061 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽) |
50 | 48, 49 | syl6sseqr 3615 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋)) |
52 | 10 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
53 | 51, 52 | sseqtrd 3604 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×t 𝐽)) |
54 | | reldisj 3972 |
. . . . . . . . . . . 12
⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
56 | | df-res 5050 |
. . . . . . . . . . . . . . 15
⊢ ( I
↾ 𝑋) = ( I ∩
(𝑋 ×
V)) |
57 | 56 | ineq2i 3773 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) |
58 | | inass 3785 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) |
59 | | inss1 3795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑) |
60 | 59, 51 | syl5ss 3579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋)) |
61 | | ssv 3588 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 ⊆ V |
62 | | xpss2 5152 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V) |
64 | 60, 63 | syl6ss 3580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V)) |
65 | | df-ss 3554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I )) |
66 | 64, 65 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I )) |
67 | 58, 66 | syl5eqr 2658 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I )) |
68 | 57, 67 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I )) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅)) |
70 | | opelxp 5070 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑎, 𝑎〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑)) |
71 | | df-br 4584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 〈𝑎, 𝑎〉 ∈ (𝑐 × 𝑑)) |
72 | | elin 3758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑)) |
73 | 70, 71, 72 | 3bitr4i 291 |
. . . . . . . . . . . . . . 15
⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
74 | 73 | notbii 309 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
75 | 74 | albii 1737 |
. . . . . . . . . . . . 13
⊢
(∀𝑎 ¬
𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
76 | | intirr 5433 |
. . . . . . . . . . . . 13
⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎) |
77 | | eq0 3888 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
78 | 75, 76, 77 | 3bitr4i 291 |
. . . . . . . . . . . 12
⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅) |
79 | 69, 78 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)) |
80 | 55, 79 | bitr3d 269 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅)) |
81 | 80 | anbi2d 736 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))) |
82 | | opelxp 5070 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
83 | 82 | anbi1i 727 |
. . . . . . . . 9
⊢
((〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
84 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)) |
85 | 81, 83, 84 | 3bitr4g 302 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) |
86 | 85 | 2rexbidva 3038 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) |
87 | 44, 86 | imbi12d 333 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
88 | 87 | 2ralbidva 2971 |
. . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ 〈𝑎, 𝑏〉 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (〈𝑎, 𝑏〉 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
89 | 33, 88 | bitrd 267 |
. . . 4
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
90 | 14, 16, 89 | 3bitrrd 294 |
. . 3
⊢ (𝐽 ∈ Top →
(∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)) ↔ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
91 | 90 | pm5.32i 667 |
. 2
⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
92 | 2, 91 | bitri 263 |
1
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾
𝑋) ∈
(Clsd‘(𝐽
×t 𝐽)))) |