MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pthaus Structured version   Visualization version   GIF version

Theorem pthaus 21663
Description: The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
pthaus ((𝐴𝑉𝐹:𝐴⟶Haus) → (∏t𝐹) ∈ Haus)

Proof of Theorem pthaus
Dummy variables 𝑘 𝑚 𝑛 𝑥 𝑦 𝑧 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 haustop 21357 . . . . 5 (𝑥 ∈ Haus → 𝑥 ∈ Top)
21ssriv 3757 . . . 4 Haus ⊆ Top
3 fss 6197 . . . 4 ((𝐹:𝐴⟶Haus ∧ Haus ⊆ Top) → 𝐹:𝐴⟶Top)
42, 3mpan2 665 . . 3 (𝐹:𝐴⟶Haus → 𝐹:𝐴⟶Top)
5 pttop 21607 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
64, 5sylan2 574 . 2 ((𝐴𝑉𝐹:𝐴⟶Haus) → (∏t𝐹) ∈ Top)
7 simprl 748 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 (∏t𝐹))
8 eqid 2771 . . . . . . . . . . 11 (∏t𝐹) = (∏t𝐹)
98ptuni 21619 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
104, 9sylan2 574 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Haus) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
1110adantr 466 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
127, 11eleqtrrd 2853 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥X𝑘𝐴 (𝐹𝑘))
13 ixpfn 8069 . . . . . . 7 (𝑥X𝑘𝐴 (𝐹𝑘) → 𝑥 Fn 𝐴)
1412, 13syl 17 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 Fn 𝐴)
15 simprr 750 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 (∏t𝐹))
1615, 11eleqtrrd 2853 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦X𝑘𝐴 (𝐹𝑘))
17 ixpfn 8069 . . . . . . 7 (𝑦X𝑘𝐴 (𝐹𝑘) → 𝑦 Fn 𝐴)
1816, 17syl 17 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 Fn 𝐴)
19 eqfnfv 6455 . . . . . 6 ((𝑥 Fn 𝐴𝑦 Fn 𝐴) → (𝑥 = 𝑦 ↔ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
2014, 18, 19syl2anc 567 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥 = 𝑦 ↔ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
2120necon3abid 2979 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥𝑦 ↔ ¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
22 rexnal 3143 . . . . 5 (∃𝑘𝐴 ¬ (𝑥𝑘) = (𝑦𝑘) ↔ ¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘))
23 df-ne 2944 . . . . . . 7 ((𝑥𝑘) ≠ (𝑦𝑘) ↔ ¬ (𝑥𝑘) = (𝑦𝑘))
24 simpllr 754 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → 𝐹:𝐴⟶Haus)
25 simprl 748 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → 𝑘𝐴)
2624, 25ffvelrnd 6504 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝐹𝑘) ∈ Haus)
27 vex 3354 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2827elixp 8070 . . . . . . . . . . . . . 14 (𝑥X𝑘𝐴 (𝐹𝑘) ↔ (𝑥 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘)))
2928simprbi 480 . . . . . . . . . . . . 13 (𝑥X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘))
3012, 29syl 17 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘))
3130r19.21bi 3081 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (𝑥𝑘) ∈ (𝐹𝑘))
3231adantrr 690 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑥𝑘) ∈ (𝐹𝑘))
33 vex 3354 . . . . . . . . . . . . . . 15 𝑦 ∈ V
3433elixp 8070 . . . . . . . . . . . . . 14 (𝑦X𝑘𝐴 (𝐹𝑘) ↔ (𝑦 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘)))
3534simprbi 480 . . . . . . . . . . . . 13 (𝑦X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘))
3616, 35syl 17 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘))
3736r19.21bi 3081 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (𝑦𝑘) ∈ (𝐹𝑘))
3837adantrr 690 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑦𝑘) ∈ (𝐹𝑘))
39 simprr 750 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑥𝑘) ≠ (𝑦𝑘))
40 eqid 2771 . . . . . . . . . . 11 (𝐹𝑘) = (𝐹𝑘)
4140hausnei 21354 . . . . . . . . . 10 (((𝐹𝑘) ∈ Haus ∧ ((𝑥𝑘) ∈ (𝐹𝑘) ∧ (𝑦𝑘) ∈ (𝐹𝑘) ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
4226, 32, 38, 39, 41syl13anc 1478 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
43 simp-4l 762 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝐴𝑉)
444ad4antlr 708 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝐹:𝐴⟶Top)
4525adantr 466 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑘𝐴)
46 eqid 2771 . . . . . . . . . . . . . . 15 (∏t𝐹) = (∏t𝐹)
4746, 8ptpjcn 21636 . . . . . . . . . . . . . 14 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝑘𝐴) → (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)))
4843, 44, 45, 47syl3anc 1476 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)))
49 simprll 758 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑚 ∈ (𝐹𝑘))
50 eqid 2771 . . . . . . . . . . . . . . 15 (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) = (𝑧 (∏t𝐹) ↦ (𝑧𝑘))
5150mptpreima 5773 . . . . . . . . . . . . . 14 ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑚) = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚}
52 cnima 21291 . . . . . . . . . . . . . 14 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑚 ∈ (𝐹𝑘)) → ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑚) ∈ (∏t𝐹))
5351, 52syl5eqelr 2855 . . . . . . . . . . . . 13 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑚 ∈ (𝐹𝑘)) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹))
5448, 49, 53syl2anc 567 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹))
55 simprlr 759 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑛 ∈ (𝐹𝑘))
5650mptpreima 5773 . . . . . . . . . . . . . 14 ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑛) = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}
57 cnima 21291 . . . . . . . . . . . . . 14 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑛 ∈ (𝐹𝑘)) → ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑛) ∈ (∏t𝐹))
5856, 57syl5eqelr 2855 . . . . . . . . . . . . 13 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑛 ∈ (𝐹𝑘)) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹))
5948, 55, 58syl2anc 567 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹))
607ad2antrr 699 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑥 (∏t𝐹))
61 simprr1 1272 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑥𝑘) ∈ 𝑚)
62 fveq1 6332 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝑧𝑘) = (𝑥𝑘))
6362eleq1d 2835 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝑧𝑘) ∈ 𝑚 ↔ (𝑥𝑘) ∈ 𝑚))
6463elrab 3516 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ↔ (𝑥 (∏t𝐹) ∧ (𝑥𝑘) ∈ 𝑚))
6560, 61, 64sylanbrc 566 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚})
6615ad2antrr 699 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑦 (∏t𝐹))
67 simprr2 1274 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑦𝑘) ∈ 𝑛)
68 fveq1 6332 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑧𝑘) = (𝑦𝑘))
6968eleq1d 2835 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝑧𝑘) ∈ 𝑛 ↔ (𝑦𝑘) ∈ 𝑛))
7069elrab 3516 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ↔ (𝑦 (∏t𝐹) ∧ (𝑦𝑘) ∈ 𝑛))
7166, 67, 70sylanbrc 566 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛})
72 inrab 4048 . . . . . . . . . . . . 13 ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = {𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)}
73 simprr3 1276 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑚𝑛) = ∅)
74 inelcm 4176 . . . . . . . . . . . . . . . . 17 (((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛) → (𝑚𝑛) ≠ ∅)
7574necon2bi 2973 . . . . . . . . . . . . . . . 16 ((𝑚𝑛) = ∅ → ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7673, 75syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7776ralrimivw 3116 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ∀𝑧 (∏t𝐹) ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
78 rabeq0 4104 . . . . . . . . . . . . . 14 ({𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)} = ∅ ↔ ∀𝑧 (∏t𝐹) ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7977, 78sylibr 224 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)} = ∅)
8072, 79syl5eq 2817 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)
81 eleq2 2839 . . . . . . . . . . . . . 14 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → (𝑥𝑢𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚}))
82 ineq1 3959 . . . . . . . . . . . . . . 15 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → (𝑢𝑣) = ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣))
8382eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → ((𝑢𝑣) = ∅ ↔ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅))
8481, 833anbi13d 1549 . . . . . . . . . . . . 13 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → ((𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦𝑣 ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅)))
85 eleq2 2839 . . . . . . . . . . . . . 14 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → (𝑦𝑣𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}))
86 ineq2 3960 . . . . . . . . . . . . . . 15 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}))
8786eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → (({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅ ↔ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅))
8885, 873anbi23d 1550 . . . . . . . . . . . . 13 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → ((𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦𝑣 ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)))
8984, 88rspc2ev 3475 . . . . . . . . . . . 12 (({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹) ∧ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹) ∧ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9054, 59, 65, 71, 80, 89syl113anc 1488 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9190expr 444 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ (𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘))) → (((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9291rexlimdvva 3186 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9342, 92mpd 15 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9493expr 444 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → ((𝑥𝑘) ≠ (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9523, 94syl5bir 233 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (¬ (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9695rexlimdva 3179 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (∃𝑘𝐴 ¬ (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9722, 96syl5bir 233 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9821, 97sylbid 230 . . 3 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9998ralrimivva 3120 . 2 ((𝐴𝑉𝐹:𝐴⟶Haus) → ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)(𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
10046ishaus 21348 . 2 ((∏t𝐹) ∈ Haus ↔ ((∏t𝐹) ∈ Top ∧ ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)(𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))))
1016, 99, 100sylanbrc 566 1 ((𝐴𝑉𝐹:𝐴⟶Haus) → (∏t𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  cin 3723  wss 3724  c0 4064   cuni 4575  cmpt 4864  ccnv 5249  cima 5253   Fn wfn 6027  wf 6028  cfv 6032  (class class class)co 6794  Xcixp 8063  tcpt 16308  Topctop 20919   Cn ccn 21250  Hauscha 21334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-map 8012  df-ixp 8064  df-en 8111  df-fin 8114  df-fi 8474  df-topgen 16313  df-pt 16314  df-top 20920  df-topon 20937  df-bases 20972  df-cn 21253  df-haus 21341
This theorem is referenced by:  poimirlem30  33773
  Copyright terms: Public domain W3C validator