| Step | Hyp | Ref
| Expression |
| 1 | | haustop 23339 |
. . . . 5
⊢ (𝑥 ∈ Haus → 𝑥 ∈ Top) |
| 2 | 1 | ssriv 3987 |
. . . 4
⊢ Haus
⊆ Top |
| 3 | | fss 6752 |
. . . 4
⊢ ((𝐹:𝐴⟶Haus ∧ Haus ⊆ Top) →
𝐹:𝐴⟶Top) |
| 4 | 2, 3 | mpan2 691 |
. . 3
⊢ (𝐹:𝐴⟶Haus → 𝐹:𝐴⟶Top) |
| 5 | | pttop 23590 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) →
(∏t‘𝐹) ∈ Top) |
| 6 | 4, 5 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) →
(∏t‘𝐹) ∈ Top) |
| 7 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 ∈ ∪
(∏t‘𝐹)) |
| 8 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
| 9 | 8 | ptuni 23602 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪
(∏t‘𝐹)) |
| 10 | 4, 9 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪
(∏t‘𝐹)) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪
(∏t‘𝐹)) |
| 12 | 7, 11 | eleqtrrd 2844 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) |
| 13 | | ixpfn 8943 |
. . . . . . 7
⊢ (𝑥 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → 𝑥 Fn 𝐴) |
| 14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 Fn 𝐴) |
| 15 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 ∈ ∪
(∏t‘𝐹)) |
| 16 | 15, 11 | eleqtrrd 2844 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) |
| 17 | | ixpfn 8943 |
. . . . . . 7
⊢ (𝑦 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → 𝑦 Fn 𝐴) |
| 18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 Fn 𝐴) |
| 19 | | eqfnfv 7051 |
. . . . . 6
⊢ ((𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) = (𝑦‘𝑘))) |
| 20 | 14, 18, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) = (𝑦‘𝑘))) |
| 21 | 20 | necon3abid 2977 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑥 ≠ 𝑦 ↔ ¬ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) = (𝑦‘𝑘))) |
| 22 | | rexnal 3100 |
. . . . 5
⊢
(∃𝑘 ∈
𝐴 ¬ (𝑥‘𝑘) = (𝑦‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) = (𝑦‘𝑘)) |
| 23 | | df-ne 2941 |
. . . . . . 7
⊢ ((𝑥‘𝑘) ≠ (𝑦‘𝑘) ↔ ¬ (𝑥‘𝑘) = (𝑦‘𝑘)) |
| 24 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → 𝐹:𝐴⟶Haus) |
| 25 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → 𝑘 ∈ 𝐴) |
| 26 | 24, 25 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → (𝐹‘𝑘) ∈ Haus) |
| 27 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 28 | 27 | elixp 8944 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↔ (𝑥 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
| 29 | 28 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 30 | 12, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 31 | 30 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑘 ∈ 𝐴) → (𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 32 | 31 | adantrr 717 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → (𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 33 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 34 | 33 | elixp 8944 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↔ (𝑦 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
| 35 | 34 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 36 | 16, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∀𝑘 ∈ 𝐴 (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 37 | 36 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑘 ∈ 𝐴) → (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 38 | 37 | adantrr 717 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
| 39 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → (𝑥‘𝑘) ≠ (𝑦‘𝑘)) |
| 40 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘) |
| 41 | 40 | hausnei 23336 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ Haus ∧ ((𝑥‘𝑘) ∈ ∪ (𝐹‘𝑘) ∧ (𝑦‘𝑘) ∈ ∪ (𝐹‘𝑘) ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → ∃𝑚 ∈ (𝐹‘𝑘)∃𝑛 ∈ (𝐹‘𝑘)((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
| 42 | 26, 32, 38, 39, 41 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → ∃𝑚 ∈ (𝐹‘𝑘)∃𝑛 ∈ (𝐹‘𝑘)((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
| 43 | | simp-4l 783 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝐴 ∈ 𝑉) |
| 44 | 4 | ad4antlr 733 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝐹:𝐴⟶Top) |
| 45 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑘 ∈ 𝐴) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ∪ (∏t‘𝐹) = ∪
(∏t‘𝐹) |
| 47 | 46, 8 | ptpjcn 23619 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘))) |
| 48 | 43, 44, 45, 47 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → (𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘))) |
| 49 | | simprll 779 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑚 ∈ (𝐹‘𝑘)) |
| 50 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ∪ (∏t‘𝐹) ↦ (𝑧‘𝑘)) = (𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) |
| 51 | 50 | mptpreima 6258 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) “ 𝑚) = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} |
| 52 | | cnima 23273 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ∪ (∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘)) ∧ 𝑚 ∈ (𝐹‘𝑘)) → (◡(𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) “ 𝑚) ∈ (∏t‘𝐹)) |
| 53 | 51, 52 | eqeltrrid 2846 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ∪ (∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘)) ∧ 𝑚 ∈ (𝐹‘𝑘)) → {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∈ (∏t‘𝐹)) |
| 54 | 48, 49, 53 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∈ (∏t‘𝐹)) |
| 55 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑛 ∈ (𝐹‘𝑘)) |
| 56 | 50 | mptpreima 6258 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) “ 𝑛) = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} |
| 57 | | cnima 23273 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ∪ (∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘)) ∧ 𝑛 ∈ (𝐹‘𝑘)) → (◡(𝑧 ∈ ∪
(∏t‘𝐹) ↦ (𝑧‘𝑘)) “ 𝑛) ∈ (∏t‘𝐹)) |
| 58 | 56, 57 | eqeltrrid 2846 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ∪ (∏t‘𝐹) ↦ (𝑧‘𝑘)) ∈ ((∏t‘𝐹) Cn (𝐹‘𝑘)) ∧ 𝑛 ∈ (𝐹‘𝑘)) → {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} ∈ (∏t‘𝐹)) |
| 59 | 48, 55, 58 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} ∈ (∏t‘𝐹)) |
| 60 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧‘𝑘) = (𝑥‘𝑘)) |
| 61 | 60 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → ((𝑧‘𝑘) ∈ 𝑚 ↔ (𝑥‘𝑘) ∈ 𝑚)) |
| 62 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑥 ∈ ∪
(∏t‘𝐹)) |
| 63 | | simprr1 1222 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → (𝑥‘𝑘) ∈ 𝑚) |
| 64 | 61, 62, 63 | elrabd 3694 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚}) |
| 65 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑧‘𝑘) = (𝑦‘𝑘)) |
| 66 | 65 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝑧‘𝑘) ∈ 𝑛 ↔ (𝑦‘𝑘) ∈ 𝑛)) |
| 67 | 15 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑦 ∈ ∪
(∏t‘𝐹)) |
| 68 | | simprr2 1223 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → (𝑦‘𝑘) ∈ 𝑛) |
| 69 | 66, 67, 68 | elrabd 3694 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → 𝑦 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) |
| 70 | | inrab 4316 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ ∪ (∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)} |
| 71 | | simprr3 1224 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → (𝑚 ∩ 𝑛) = ∅) |
| 72 | | inelcm 4465 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛) → (𝑚 ∩ 𝑛) ≠ ∅) |
| 73 | 72 | necon2bi 2971 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∩ 𝑛) = ∅ → ¬ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)) |
| 74 | 71, 73 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → ¬ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)) |
| 75 | 74 | ralrimivw 3150 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → ∀𝑧 ∈ ∪ (∏t‘𝐹) ¬ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)) |
| 76 | | rabeq0 4388 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ ∪ (∏t‘𝐹) ∣ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)} = ∅ ↔ ∀𝑧 ∈ ∪ (∏t‘𝐹) ¬ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)) |
| 77 | 75, 76 | sylibr 234 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → {𝑧 ∈ ∪
(∏t‘𝐹) ∣ ((𝑧‘𝑘) ∈ 𝑚 ∧ (𝑧‘𝑘) ∈ 𝑛)} = ∅) |
| 78 | 70, 77 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) = ∅) |
| 79 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚})) |
| 80 | | ineq1 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} → (𝑢 ∩ 𝑣) = ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣)) |
| 81 | 80 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} → ((𝑢 ∩ 𝑣) = ∅ ↔ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣) = ∅)) |
| 82 | 79, 81 | 3anbi13d 1440 |
. . . . . . . . . . . . 13
⊢ (𝑢 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} → ((𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∧ 𝑦 ∈ 𝑣 ∧ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣) = ∅))) |
| 83 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛})) |
| 84 | | ineq2 4214 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} → ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣) = ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛})) |
| 85 | 84 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} → (({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣) = ∅ ↔ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) = ∅)) |
| 86 | 83, 85 | 3anbi23d 1441 |
. . . . . . . . . . . . 13
⊢ (𝑣 = {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} → ((𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∧ 𝑦 ∈ 𝑣 ∧ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ 𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} ∧ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) = ∅))) |
| 87 | 82, 86 | rspc2ev 3635 |
. . . . . . . . . . . 12
⊢ (({𝑧 ∈ ∪ (∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∈ (∏t‘𝐹) ∧ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} ∈ (∏t‘𝐹) ∧ (𝑥 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛} ∧ ({𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑚} ∩ {𝑧 ∈ ∪
(∏t‘𝐹) ∣ (𝑧‘𝑘) ∈ 𝑛}) = ∅)) → ∃𝑢 ∈
(∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)) |
| 88 | 54, 59, 64, 69, 78, 87 | syl113anc 1384 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ ((𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘)) ∧ ((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) → ∃𝑢 ∈
(∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)) |
| 89 | 88 | expr 456 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) ∧ (𝑚 ∈ (𝐹‘𝑘) ∧ 𝑛 ∈ (𝐹‘𝑘))) → (((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 90 | 89 | rexlimdvva 3213 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → (∃𝑚 ∈ (𝐹‘𝑘)∃𝑛 ∈ (𝐹‘𝑘)((𝑥‘𝑘) ∈ 𝑚 ∧ (𝑦‘𝑘) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 91 | 42, 90 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑘 ∈ 𝐴 ∧ (𝑥‘𝑘) ≠ (𝑦‘𝑘))) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)) |
| 92 | 91 | expr 456 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑘 ∈ 𝐴) → ((𝑥‘𝑘) ≠ (𝑦‘𝑘) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 93 | 23, 92 | biimtrrid 243 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑘 ∈ 𝐴) → (¬ (𝑥‘𝑘) = (𝑦‘𝑘) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 94 | 93 | rexlimdva 3155 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (∃𝑘 ∈ 𝐴 ¬ (𝑥‘𝑘) = (𝑦‘𝑘) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 95 | 22, 94 | biimtrrid 243 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (¬ ∀𝑘 ∈ 𝐴 (𝑥‘𝑘) = (𝑦‘𝑘) → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 96 | 21, 95 | sylbid 240 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑥 ≠ 𝑦 → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 97 | 96 | ralrimivva 3202 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → ∀𝑥 ∈ ∪ (∏t‘𝐹)∀𝑦 ∈ ∪
(∏t‘𝐹)(𝑥 ≠ 𝑦 → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))) |
| 98 | 46 | ishaus 23330 |
. 2
⊢
((∏t‘𝐹) ∈ Haus ↔
((∏t‘𝐹) ∈ Top ∧ ∀𝑥 ∈ ∪ (∏t‘𝐹)∀𝑦 ∈ ∪
(∏t‘𝐹)(𝑥 ≠ 𝑦 → ∃𝑢 ∈ (∏t‘𝐹)∃𝑣 ∈ (∏t‘𝐹)(𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))) |
| 99 | 6, 97, 98 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) →
(∏t‘𝐹) ∈ Haus) |