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

Theorem pthaus 21724
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 21418 . . . . 5 (𝑥 ∈ Haus → 𝑥 ∈ Top)
21ssriv 3767 . . . 4 Haus ⊆ Top
3 fss 6238 . . . 4 ((𝐹:𝐴⟶Haus ∧ Haus ⊆ Top) → 𝐹:𝐴⟶Top)
42, 3mpan2 682 . . 3 (𝐹:𝐴⟶Haus → 𝐹:𝐴⟶Top)
5 pttop 21668 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
64, 5sylan2 586 . 2 ((𝐴𝑉𝐹:𝐴⟶Haus) → (∏t𝐹) ∈ Top)
7 simprl 787 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 (∏t𝐹))
8 eqid 2765 . . . . . . . . . . 11 (∏t𝐹) = (∏t𝐹)
98ptuni 21680 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
104, 9sylan2 586 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Haus) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
1110adantr 472 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
127, 11eleqtrrd 2847 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥X𝑘𝐴 (𝐹𝑘))
13 ixpfn 8121 . . . . . . 7 (𝑥X𝑘𝐴 (𝐹𝑘) → 𝑥 Fn 𝐴)
1412, 13syl 17 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 Fn 𝐴)
15 simprr 789 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 (∏t𝐹))
1615, 11eleqtrrd 2847 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦X𝑘𝐴 (𝐹𝑘))
17 ixpfn 8121 . . . . . . 7 (𝑦X𝑘𝐴 (𝐹𝑘) → 𝑦 Fn 𝐴)
1816, 17syl 17 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 Fn 𝐴)
19 eqfnfv 6503 . . . . . 6 ((𝑥 Fn 𝐴𝑦 Fn 𝐴) → (𝑥 = 𝑦 ↔ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
2014, 18, 19syl2anc 579 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥 = 𝑦 ↔ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
2120necon3abid 2973 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥𝑦 ↔ ¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘)))
22 rexnal 3141 . . . . 5 (∃𝑘𝐴 ¬ (𝑥𝑘) = (𝑦𝑘) ↔ ¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘))
23 df-ne 2938 . . . . . . 7 ((𝑥𝑘) ≠ (𝑦𝑘) ↔ ¬ (𝑥𝑘) = (𝑦𝑘))
24 simpllr 793 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → 𝐹:𝐴⟶Haus)
25 simprl 787 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → 𝑘𝐴)
2624, 25ffvelrnd 6552 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝐹𝑘) ∈ Haus)
27 vex 3353 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2827elixp 8122 . . . . . . . . . . . . . 14 (𝑥X𝑘𝐴 (𝐹𝑘) ↔ (𝑥 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘)))
2928simprbi 490 . . . . . . . . . . . . 13 (𝑥X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘))
3012, 29syl 17 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑘𝐴 (𝑥𝑘) ∈ (𝐹𝑘))
3130r19.21bi 3079 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (𝑥𝑘) ∈ (𝐹𝑘))
3231adantrr 708 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑥𝑘) ∈ (𝐹𝑘))
33 vex 3353 . . . . . . . . . . . . . . 15 𝑦 ∈ V
3433elixp 8122 . . . . . . . . . . . . . 14 (𝑦X𝑘𝐴 (𝐹𝑘) ↔ (𝑦 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘)))
3534simprbi 490 . . . . . . . . . . . . 13 (𝑦X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘))
3616, 35syl 17 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑘𝐴 (𝑦𝑘) ∈ (𝐹𝑘))
3736r19.21bi 3079 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (𝑦𝑘) ∈ (𝐹𝑘))
3837adantrr 708 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑦𝑘) ∈ (𝐹𝑘))
39 simprr 789 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (𝑥𝑘) ≠ (𝑦𝑘))
40 eqid 2765 . . . . . . . . . . 11 (𝐹𝑘) = (𝐹𝑘)
4140hausnei 21415 . . . . . . . . . 10 (((𝐹𝑘) ∈ Haus ∧ ((𝑥𝑘) ∈ (𝐹𝑘) ∧ (𝑦𝑘) ∈ (𝐹𝑘) ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
4226, 32, 38, 39, 41syl13anc 1491 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))
43 simp-4l 801 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝐴𝑉)
444ad4antlr 726 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝐹:𝐴⟶Top)
4525adantr 472 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑘𝐴)
46 eqid 2765 . . . . . . . . . . . . . . 15 (∏t𝐹) = (∏t𝐹)
4746, 8ptpjcn 21697 . . . . . . . . . . . . . 14 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝑘𝐴) → (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)))
4843, 44, 45, 47syl3anc 1490 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)))
49 simprll 797 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑚 ∈ (𝐹𝑘))
50 eqid 2765 . . . . . . . . . . . . . . 15 (𝑧 (∏t𝐹) ↦ (𝑧𝑘)) = (𝑧 (∏t𝐹) ↦ (𝑧𝑘))
5150mptpreima 5816 . . . . . . . . . . . . . 14 ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑚) = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚}
52 cnima 21352 . . . . . . . . . . . . . 14 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑚 ∈ (𝐹𝑘)) → ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑚) ∈ (∏t𝐹))
5351, 52syl5eqelr 2849 . . . . . . . . . . . . 13 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑚 ∈ (𝐹𝑘)) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹))
5448, 49, 53syl2anc 579 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹))
55 simprlr 798 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑛 ∈ (𝐹𝑘))
5650mptpreima 5816 . . . . . . . . . . . . . 14 ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑛) = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}
57 cnima 21352 . . . . . . . . . . . . . 14 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑛 ∈ (𝐹𝑘)) → ((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) “ 𝑛) ∈ (∏t𝐹))
5856, 57syl5eqelr 2849 . . . . . . . . . . . . 13 (((𝑧 (∏t𝐹) ↦ (𝑧𝑘)) ∈ ((∏t𝐹) Cn (𝐹𝑘)) ∧ 𝑛 ∈ (𝐹𝑘)) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹))
5948, 55, 58syl2anc 579 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹))
607ad2antrr 717 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑥 (∏t𝐹))
61 simprr1 1287 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑥𝑘) ∈ 𝑚)
62 fveq1 6376 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝑧𝑘) = (𝑥𝑘))
6362eleq1d 2829 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝑧𝑘) ∈ 𝑚 ↔ (𝑥𝑘) ∈ 𝑚))
6463elrab 3521 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ↔ (𝑥 (∏t𝐹) ∧ (𝑥𝑘) ∈ 𝑚))
6560, 61, 64sylanbrc 578 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚})
6615ad2antrr 717 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑦 (∏t𝐹))
67 simprr2 1289 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑦𝑘) ∈ 𝑛)
68 fveq1 6376 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑧𝑘) = (𝑦𝑘))
6968eleq1d 2829 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝑧𝑘) ∈ 𝑛 ↔ (𝑦𝑘) ∈ 𝑛))
7069elrab 3521 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ↔ (𝑦 (∏t𝐹) ∧ (𝑦𝑘) ∈ 𝑛))
7166, 67, 70sylanbrc 578 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛})
72 inrab 4065 . . . . . . . . . . . . 13 ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = {𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)}
73 simprr3 1291 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → (𝑚𝑛) = ∅)
74 inelcm 4195 . . . . . . . . . . . . . . . . 17 (((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛) → (𝑚𝑛) ≠ ∅)
7574necon2bi 2967 . . . . . . . . . . . . . . . 16 ((𝑚𝑛) = ∅ → ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7673, 75syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7776ralrimivw 3114 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ∀𝑧 (∏t𝐹) ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
78 rabeq0 4123 . . . . . . . . . . . . . 14 ({𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)} = ∅ ↔ ∀𝑧 (∏t𝐹) ¬ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛))
7977, 78sylibr 225 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → {𝑧 (∏t𝐹) ∣ ((𝑧𝑘) ∈ 𝑚 ∧ (𝑧𝑘) ∈ 𝑛)} = ∅)
8072, 79syl5eq 2811 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)
81 eleq2 2833 . . . . . . . . . . . . . 14 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → (𝑥𝑢𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚}))
82 ineq1 3971 . . . . . . . . . . . . . . 15 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → (𝑢𝑣) = ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣))
8382eqeq1d 2767 . . . . . . . . . . . . . 14 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → ((𝑢𝑣) = ∅ ↔ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅))
8481, 833anbi13d 1562 . . . . . . . . . . . . 13 (𝑢 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} → ((𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦𝑣 ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅)))
85 eleq2 2833 . . . . . . . . . . . . . 14 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → (𝑦𝑣𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}))
86 ineq2 3972 . . . . . . . . . . . . . . 15 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}))
8786eqeq1d 2767 . . . . . . . . . . . . . 14 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → (({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅ ↔ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅))
8885, 873anbi23d 1563 . . . . . . . . . . . . 13 (𝑣 = {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} → ((𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦𝑣 ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ 𝑣) = ∅) ↔ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)))
8984, 88rspc2ev 3477 . . . . . . . . . . . 12 (({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∈ (∏t𝐹) ∧ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∈ (∏t𝐹) ∧ (𝑥 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∧ 𝑦 ∈ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛} ∧ ({𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑚} ∩ {𝑧 (∏t𝐹) ∣ (𝑧𝑘) ∈ 𝑛}) = ∅)) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9054, 59, 65, 71, 80, 89syl113anc 1501 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ ((𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘)) ∧ ((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅))) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9190expr 448 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) ∧ (𝑚 ∈ (𝐹𝑘) ∧ 𝑛 ∈ (𝐹𝑘))) → (((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9291rexlimdvva 3185 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → (∃𝑚 ∈ (𝐹𝑘)∃𝑛 ∈ (𝐹𝑘)((𝑥𝑘) ∈ 𝑚 ∧ (𝑦𝑘) ∈ 𝑛 ∧ (𝑚𝑛) = ∅) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9342, 92mpd 15 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑘𝐴 ∧ (𝑥𝑘) ≠ (𝑦𝑘))) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))
9493expr 448 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → ((𝑥𝑘) ≠ (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9523, 94syl5bir 234 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑘𝐴) → (¬ (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9695rexlimdva 3178 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (∃𝑘𝐴 ¬ (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9722, 96syl5bir 234 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (¬ ∀𝑘𝐴 (𝑥𝑘) = (𝑦𝑘) → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9821, 97sylbid 231 . . 3 (((𝐴𝑉𝐹:𝐴⟶Haus) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
9998ralrimivva 3118 . 2 ((𝐴𝑉𝐹:𝐴⟶Haus) → ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)(𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅)))
10046ishaus 21409 . 2 ((∏t𝐹) ∈ Haus ↔ ((∏t𝐹) ∈ Top ∧ ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)(𝑥𝑦 → ∃𝑢 ∈ (∏t𝐹)∃𝑣 ∈ (∏t𝐹)(𝑥𝑢𝑦𝑣 ∧ (𝑢𝑣) = ∅))))
1016, 99, 100sylanbrc 578 1 ((𝐴𝑉𝐹:𝐴⟶Haus) → (∏t𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cin 3733  wss 3734  c0 4081   cuni 4596  cmpt 4890  ccnv 5278  cima 5282   Fn wfn 6065  wf 6066  cfv 6070  (class class class)co 6844  Xcixp 8115  tcpt 16368  Topctop 20980   Cn ccn 21311  Hauscha 21395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-er 7949  df-map 8064  df-ixp 8116  df-en 8163  df-fin 8166  df-fi 8526  df-topgen 16373  df-pt 16374  df-top 20981  df-topon 20998  df-bases 21033  df-cn 21314  df-haus 21402
This theorem is referenced by:  poimirlem30  33866
  Copyright terms: Public domain W3C validator