Step | Hyp | Ref
| Expression |
1 | | hausdiag.x |
. . 3
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | ishaus 22696 |
. 2
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
3 | | txtop 22943 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
4 | 3 | anidms 568 |
. . . . 5
⊢ (𝐽 ∈ Top → (𝐽 ×t 𝐽) ∈ Top) |
5 | | idssxp 6006 |
. . . . . 6
⊢ ( I
↾ 𝑋) ⊆ (𝑋 × 𝑋) |
6 | 1, 1 | txuni 22966 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
7 | 6 | anidms 568 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
8 | 5, 7 | sseqtrid 4000 |
. . . . 5
⊢ (𝐽 ∈ Top → ( I ↾
𝑋) ⊆ ∪ (𝐽
×t 𝐽)) |
9 | | eqid 2733 |
. . . . . 6
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
10 | 9 | iscld2 22402 |
. . . . 5
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ( I ↾
𝑋) ⊆ ∪ (𝐽
×t 𝐽))
→ (( I ↾ 𝑋)
∈ (Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×t 𝐽))) |
11 | 4, 8, 10 | syl2anc 585 |
. . . 4
⊢ (𝐽 ∈ Top → (( I ↾
𝑋) ∈
(Clsd‘(𝐽
×t 𝐽))
↔ (∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×t 𝐽))) |
12 | | eltx 22942 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
∈ (𝐽
×t 𝐽)
↔ ∀𝑒 ∈
(∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
13 | 12 | anidms 568 |
. . . 4
⊢ (𝐽 ∈ Top → ((∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
∈ (𝐽
×t 𝐽)
↔ ∀𝑒 ∈
(∪ (𝐽 ×t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
14 | | eldif 3924 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
↔ (𝑒 ∈ ∪ (𝐽
×t 𝐽)
∧ ¬ 𝑒 ∈ ( I
↾ 𝑋))) |
15 | 7 | eqcomd 2739 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top → ∪ (𝐽
×t 𝐽) =
(𝑋 × 𝑋)) |
16 | 15 | eleq2d 2820 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽
×t 𝐽)
↔ 𝑒 ∈ (𝑋 × 𝑋))) |
17 | 16 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽
×t 𝐽)
∧ ¬ 𝑒 ∈ ( I
↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))) |
18 | 14, 17 | bitrid 283 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))) |
19 | 18 | imbi1d 342 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
→ ∃𝑐 ∈
𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
20 | | impexp 452 |
. . . . . . . 8
⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
21 | 19, 20 | bitrdi 287 |
. . . . . . 7
⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))
→ ∃𝑐 ∈
𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))))) |
22 | 21 | ralbidv2 3167 |
. . . . . 6
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
23 | | eleq1 2822 |
. . . . . . . . 9
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋))) |
24 | 23 | notbid 318 |
. . . . . . . 8
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋))) |
25 | | eleq1 2822 |
. . . . . . . . . 10
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑))) |
26 | 25 | anbi1d 631 |
. . . . . . . . 9
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
27 | 26 | 2rexbidv 3210 |
. . . . . . . 8
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
28 | 24, 27 | imbi12d 345 |
. . . . . . 7
⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (¬
⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
29 | 28 | ralxp 5801 |
. . . . . 6
⊢
(∀𝑒 ∈
(𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))))) |
30 | 22, 29 | bitrdi 287 |
. . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))))) |
31 | | vex 3451 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
32 | 31 | opelresi 5949 |
. . . . . . . . . 10
⊢
(⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )) |
33 | | ibar 530 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))) |
34 | 33 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))) |
35 | | df-br 5110 |
. . . . . . . . . . . 12
⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I ) |
36 | 31 | ideq 5812 |
. . . . . . . . . . . 12
⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏) |
37 | 35, 36 | bitr3i 277 |
. . . . . . . . . . 11
⊢
(⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏) |
38 | 34, 37 | bitr3di 286 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ) ↔ 𝑎 = 𝑏)) |
39 | 32, 38 | bitrid 283 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏)) |
40 | 39 | adantl 483 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏)) |
41 | 40 | necon3bbid 2978 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏)) |
42 | | elssuni 4902 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽) |
43 | | elssuni 4902 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽) |
44 | | xpss12 5652 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ⊆ ∪ 𝐽
∧ 𝑑 ⊆ ∪ 𝐽)
→ (𝑐 × 𝑑) ⊆ (∪ 𝐽
× ∪ 𝐽)) |
45 | 42, 43, 44 | syl2an 597 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽)) |
46 | 1, 1 | xpeq12i 5665 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽) |
47 | 45, 46 | sseqtrrdi 3999 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋)) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋)) |
49 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
50 | 48, 49 | sseqtrd 3988 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×t 𝐽)) |
51 | | reldisj 4415 |
. . . . . . . . . . . 12
⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
53 | | df-res 5649 |
. . . . . . . . . . . . . . 15
⊢ ( I
↾ 𝑋) = ( I ∩
(𝑋 ×
V)) |
54 | 53 | ineq2i 4173 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) |
55 | | inass 4183 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) |
56 | | inss1 4192 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑) |
57 | 56, 48 | sstrid 3959 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋)) |
58 | | ssv 3972 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 ⊆ V |
59 | | xpss2 5657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V)) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V) |
61 | 57, 60 | sstrdi 3960 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V)) |
62 | | df-ss 3931 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I )) |
63 | 61, 62 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I )) |
64 | 55, 63 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I )) |
65 | 54, 64 | eqtrid 2785 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I )) |
66 | 65 | eqeq1d 2735 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅)) |
67 | | opelxp 5673 |
. . . . . . . . . . . . . . . 16
⊢
(⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑)) |
68 | | df-br 5110 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑)) |
69 | | elin 3930 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑)) |
70 | 67, 68, 69 | 3bitr4i 303 |
. . . . . . . . . . . . . . 15
⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
71 | 70 | notbii 320 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
72 | 71 | albii 1822 |
. . . . . . . . . . . . 13
⊢
(∀𝑎 ¬
𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
73 | | intirr 6076 |
. . . . . . . . . . . . 13
⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎) |
74 | | eq0 4307 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑)) |
75 | 72, 73, 74 | 3bitr4i 303 |
. . . . . . . . . . . 12
⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅) |
76 | 66, 75 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)) |
77 | 52, 76 | bitr3d 281 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅)) |
78 | 77 | anbi2d 630 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))) |
79 | | opelxp 5673 |
. . . . . . . . . 10
⊢
(⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑)) |
80 | 79 | anbi1i 625 |
. . . . . . . . 9
⊢
((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) |
81 | | df-3an 1090 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)) |
82 | 78, 80, 81 | 3bitr4g 314 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) |
83 | 82 | 2rexbidva 3208 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) |
84 | 41, 83 | imbi12d 345 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
85 | 84 | 2ralbidva 3207 |
. . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
86 | 30, 85 | bitrd 279 |
. . . 4
⊢ (𝐽 ∈ Top →
(∀𝑒 ∈ (∪ (𝐽
×t 𝐽)
∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪
(𝐽 ×t
𝐽) ∖ ( I ↾
𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))) |
87 | 11, 13, 86 | 3bitrrd 306 |
. . 3
⊢ (𝐽 ∈ Top →
(∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)) ↔ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
88 | 87 | pm5.32i 576 |
. 2
⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
89 | 2, 88 | bitri 275 |
1
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾
𝑋) ∈
(Clsd‘(𝐽
×t 𝐽)))) |