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

Theorem hauscmplem 22757
Description: Lemma for hauscmp 22758. (Contributed by Mario Carneiro, 27-Nov-2013.)
Hypotheses
Ref Expression
hauscmp.1 𝑋 = 𝐽
hauscmplem.2 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
hauscmplem.3 (𝜑𝐽 ∈ Haus)
hauscmplem.4 (𝜑𝑆𝑋)
hauscmplem.5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
hauscmplem.6 (𝜑𝐴 ∈ (𝑋𝑆))
Assertion
Ref Expression
hauscmplem (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
Distinct variable groups:   𝑦,𝑤,𝑧,𝐴   𝑤,𝐽,𝑦,𝑧   𝜑,𝑤,𝑦,𝑧   𝑤,𝑆,𝑦,𝑧   𝑧,𝑂   𝑤,𝑋,𝑦,𝑧
Allowed substitution hints:   𝑂(𝑦,𝑤)

Proof of Theorem hauscmplem
Dummy variables 𝑓 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hauscmplem.3 . . . . . . 7 (𝜑𝐽 ∈ Haus)
2 haustop 22682 . . . . . . 7 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
43ad3antrrr 728 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5 hauscmp.1 . . . . . 6 𝑋 = 𝐽
65topopn 22255 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
74, 6syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑋𝐽)
8 hauscmplem.6 . . . . . 6 (𝜑𝐴 ∈ (𝑋𝑆))
98eldifad 3922 . . . . 5 (𝜑𝐴𝑋)
109ad3antrrr 728 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐴𝑋)
115clstop 22420 . . . . . . 7 (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
124, 11syl 17 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13 simplr 767 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 𝑥)
14 unieq 4876 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
15 uni0 4896 . . . . . . . . . . . 12 ∅ = ∅
1614, 15eqtrdi 2792 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1716adantl 482 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑥 = ∅)
1813, 17sseqtrd 3984 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19 ss0 4358 . . . . . . . . 9 (𝑆 ⊆ ∅ → 𝑆 = ∅)
2018, 19syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
2120difeq2d 4082 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = (𝑋 ∖ ∅))
22 dif0 4332 . . . . . . 7 (𝑋 ∖ ∅) = 𝑋
2321, 22eqtrdi 2792 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = 𝑋)
2412, 23eqtr4d 2779 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋𝑆))
25 eqimss 4000 . . . . 5 (((cls‘𝐽)‘𝑋) = (𝑋𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
2624, 25syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
27 eleq2 2826 . . . . . 6 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
28 fveq2 6842 . . . . . . 7 (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
2928sseq1d 3975 . . . . . 6 (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆)))
3027, 29anbi12d 631 . . . . 5 (𝑧 = 𝑋 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))))
3130rspcev 3581 . . . 4 ((𝑋𝐽 ∧ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
327, 10, 26, 31syl12anc 835 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
33 elin 3926 . . . . . . 7 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin))
34 id 22 . . . . . . . 8 (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35 elpwi 4567 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑂𝑥𝑂)
3635sseld 3943 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥𝑧𝑂))
37 difeq2 4076 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑋𝑦) = (𝑋𝑧))
3837sseq2d 3976 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
3938anbi2d 629 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4039rexbidv 3175 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
41 hauscmplem.2 . . . . . . . . . . . 12 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
4240, 41elrab2 3648 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑧𝐽 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4342simprbi 497 . . . . . . . . . 10 (𝑧𝑂 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
4436, 43syl6 35 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4544ralrimiv 3142 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑂 → ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
46 eleq2 2826 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (𝐴𝑤𝐴 ∈ (𝑓𝑧)))
47 fveq2 6842 . . . . . . . . . . 11 (𝑤 = (𝑓𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓𝑧)))
4847sseq1d 3975 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧) ↔ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))
4946, 48anbi12d 631 . . . . . . . . 9 (𝑤 = (𝑓𝑧) → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)) ↔ (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5049ac6sfi 9231 . . . . . . . 8 ((𝑥 ∈ Fin ∧ ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5134, 45, 50syl2anr 597 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5233, 51sylbi 216 . . . . . 6 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5352ad2antlr 725 . . . . 5 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
543ad3antrrr 728 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐽 ∈ Top)
55 frn 6675 . . . . . . . 8 (𝑓:𝑥𝐽 → ran 𝑓𝐽)
5655ad2antrl 726 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
57 simprr 771 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58 simpl 483 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥𝐽)
59 fdm 6677 . . . . . . . . . . . 12 (𝑓:𝑥𝐽 → dom 𝑓 = 𝑥)
6059eqeq1d 2738 . . . . . . . . . . 11 (𝑓:𝑥𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
61 dm0rn0 5880 . . . . . . . . . . 11 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
6260, 61bitr3di 285 . . . . . . . . . 10 (𝑓:𝑥𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
6362necon3bid 2988 . . . . . . . . 9 (𝑓:𝑥𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
6463biimpac 479 . . . . . . . 8 ((𝑥 ≠ ∅ ∧ 𝑓:𝑥𝐽) → ran 𝑓 ≠ ∅)
6557, 58, 64syl2an 596 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ≠ ∅)
6633simprbi 497 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
6766ad2antlr 725 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68 ffn 6668 . . . . . . . . . 10 (𝑓:𝑥𝐽𝑓 Fn 𝑥)
69 dffn4 6762 . . . . . . . . . 10 (𝑓 Fn 𝑥𝑓:𝑥onto→ran 𝑓)
7068, 69sylib 217 . . . . . . . . 9 (𝑓:𝑥𝐽𝑓:𝑥onto→ran 𝑓)
7170adantr 481 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥onto→ran 𝑓)
72 fofi 9282 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝑓:𝑥onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7367, 71, 72syl2an 596 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ∈ Fin)
74 fiinopn 22250 . . . . . . . 8 (𝐽 ∈ Top → ((ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝐽))
7574imp 407 . . . . . . 7 ((𝐽 ∈ Top ∧ (ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝐽)
7654, 56, 65, 73, 75syl13anc 1372 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
77 simpl 483 . . . . . . . . . 10 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝐴 ∈ (𝑓𝑧))
7877ralimi 3086 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
7978ad2antll 727 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
808ad3antrrr 728 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ∈ (𝑋𝑆))
81 eliin 4959 . . . . . . . . 9 (𝐴 ∈ (𝑋𝑆) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8280, 81syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8379, 82mpbird 256 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 𝑧𝑥 (𝑓𝑧))
8468ad2antrl 726 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑓 Fn 𝑥)
85 fnrnfv 6902 . . . . . . . . . 10 (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
8685inteqd 4912 . . . . . . . . 9 (𝑓 Fn 𝑥 ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
87 fvex 6855 . . . . . . . . . 10 (𝑓𝑧) ∈ V
8887dfiin2 4994 . . . . . . . . 9 𝑧𝑥 (𝑓𝑧) = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)}
8986, 88eqtr4di 2794 . . . . . . . 8 (𝑓 Fn 𝑥 ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9084, 89syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9183, 90eleqtrrd 2841 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ran 𝑓)
9257adantr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑥 ≠ ∅)
933ad4antr 730 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → 𝐽 ∈ Top)
94 ffvelcdm 7032 . . . . . . . . . . . . . . 15 ((𝑓:𝑥𝐽𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
9594adantll 712 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
96 elssuni 4898 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝐽 → (𝑓𝑧) ⊆ 𝐽)
9795, 96syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝐽)
9897, 5sseqtrrdi 3995 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝑋)
995clscld 22398 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10093, 98, 99syl2anc 584 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
101100ralrimiva 3143 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
102101adantrr 715 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
103 iincld 22390 . . . . . . . . 9 ((𝑥 ≠ ∅ ∧ ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10492, 102, 103syl2anc 584 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
1055sscls 22407 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
10693, 98, 105syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
107106ralrimiva 3143 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
108 ssel 3937 . . . . . . . . . . . . . 14 ((𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 ∈ (𝑓𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
109108ral2imi 3088 . . . . . . . . . . . . 13 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (∀𝑧𝑥 𝑦 ∈ (𝑓𝑧) → ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
110 eliin 4959 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧)))
111110elv 3451 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧))
112 eliin 4959 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
113112elv 3451 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)))
114109, 111, 1133imtr4g 295 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 𝑧𝑥 (𝑓𝑧) → 𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))))
115114ssrdv 3950 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
116107, 115syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
117116adantrr 715 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
11890, 117eqsstrd 3982 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
1195clsss2 22423 . . . . . . . 8 (( 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽) ∧ ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
120104, 118, 119syl2anc 584 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
121 ssel 3937 . . . . . . . . . . . . 13 (((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
122121adantl 482 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
123122ral2imi 3088 . . . . . . . . . . 11 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
124 eliin 4959 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
125124elv 3451 . . . . . . . . . . 11 (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧))
126123, 113, 1253imtr4g 295 . . . . . . . . . 10 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 𝑧𝑥 (𝑋𝑧)))
127126ssrdv 3950 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
128127ad2antll 727 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
129 iindif2 5037 . . . . . . . . . 10 (𝑥 ≠ ∅ → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
13092, 129syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
131 simplrl 775 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑆 𝑥)
132 uniiun 5018 . . . . . . . . . . . 12 𝑥 = 𝑧𝑥 𝑧
133132sseq2i 3973 . . . . . . . . . . 11 (𝑆 𝑥𝑆 𝑧𝑥 𝑧)
134 sscon 4098 . . . . . . . . . . 11 (𝑆 𝑧𝑥 𝑧 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
135133, 134sylbi 216 . . . . . . . . . 10 (𝑆 𝑥 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
136131, 135syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
137130, 136eqsstrd 3982 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) ⊆ (𝑋𝑆))
138128, 137sstrd 3954 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑆))
139120, 138sstrd 3954 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))
140 eleq2 2826 . . . . . . . 8 (𝑧 = ran 𝑓 → (𝐴𝑧𝐴 ran 𝑓))
141 fveq2 6842 . . . . . . . . 9 (𝑧 = ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘ ran 𝑓))
142141sseq1d 3975 . . . . . . . 8 (𝑧 = ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆)))
143140, 142anbi12d 631 . . . . . . 7 (𝑧 = ran 𝑓 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))))
144143rspcev 3581 . . . . . 6 (( ran 𝑓𝐽 ∧ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14576, 91, 139, 144syl12anc 835 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14653, 145exlimddv 1938 . . . 4 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
147146anassrs 468 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14832, 147pm2.61dane 3032 . 2 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
1491adantr 481 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐽 ∈ Haus)
150 hauscmplem.4 . . . . . . . . 9 (𝜑𝑆𝑋)
151150sselda 3944 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝑋)
1529adantr 481 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴𝑋)
153 id 22 . . . . . . . . 9 (𝑥𝑆𝑥𝑆)
1548eldifbd 3923 . . . . . . . . 9 (𝜑 → ¬ 𝐴𝑆)
155 nelne2 3042 . . . . . . . . 9 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
156153, 154, 155syl2anr 597 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝐴)
1575hausnei 22679 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥𝑋𝐴𝑋𝑥𝐴)) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
158149, 151, 152, 156, 157syl13anc 1372 . . . . . . 7 ((𝜑𝑥𝑆) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
159 3anass 1095 . . . . . . . . . . 11 ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) ↔ (𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)))
160 elssuni 4898 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤 𝐽)
161160, 5sseqtrrdi 3995 . . . . . . . . . . . . . . . 16 (𝑤𝐽𝑤𝑋)
162161adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → 𝑤𝑋)
163 incom 4161 . . . . . . . . . . . . . . . . 17 (𝑦𝑤) = (𝑤𝑦)
164163eqeq1i 2741 . . . . . . . . . . . . . . . 16 ((𝑦𝑤) = ∅ ↔ (𝑤𝑦) = ∅)
165 reldisj 4411 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑤𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
166164, 165bitrid 282 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
167162, 166syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
168149, 2syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐽 ∈ Top)
1695opncld 22384 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
170168, 169sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
171170adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
1725clsss2 22423 . . . . . . . . . . . . . . . 16 (((𝑋𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))
173172ex 413 . . . . . . . . . . . . . . 15 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
174171, 173syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
175167, 174sylbid 239 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
176175anim2d 612 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
177176anim2d 612 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
178159, 177biimtrid 241 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
179178reximdva 3165 . . . . . . . . 9 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
180 r19.42v 3187 . . . . . . . . 9 (∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))) ↔ (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
181179, 180syl6ib 250 . . . . . . . 8 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
182181reximdva 3165 . . . . . . 7 ((𝜑𝑥𝑆) → (∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
183158, 182mpd 15 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
18441unieqi 4878 . . . . . . . 8 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
185184eleq2i 2829 . . . . . . 7 (𝑥 𝑂𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))})
186 elunirab 4881 . . . . . . 7 (𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
187185, 186bitri 274 . . . . . 6 (𝑥 𝑂 ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
188183, 187sylibr 233 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 𝑂)
189188ex 413 . . . 4 (𝜑 → (𝑥𝑆𝑥 𝑂))
190189ssrdv 3950 . . 3 (𝜑𝑆 𝑂)
191 unieq 4876 . . . . . 6 (𝑧 = 𝑂 𝑧 = 𝑂)
192191sseq2d 3976 . . . . 5 (𝑧 = 𝑂 → (𝑆 𝑧𝑆 𝑂))
193 pweq 4574 . . . . . . 7 (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
194193ineq1d 4171 . . . . . 6 (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
195194rexeqdv 3314 . . . . 5 (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
196192, 195imbi12d 344 . . . 4 (𝑧 = 𝑂 → ((𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥) ↔ (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)))
197 hauscmplem.5 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
1985cmpsub 22751 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)))
199198biimp3a 1469 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ (𝐽t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
2003, 150, 197, 199syl3anc 1371 . . . 4 (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
20141ssrab3 4040 . . . . 5 𝑂𝐽
202 elpw2g 5301 . . . . . 6 (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
2031, 202syl 17 . . . . 5 (𝜑 → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
204201, 203mpbiri 257 . . . 4 (𝜑𝑂 ∈ 𝒫 𝐽)
205196, 200, 204rspcdva 3582 . . 3 (𝜑 → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
206190, 205mpd 15 . 2 (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)
207148, 206r19.29a 3159 1 (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560   cuni 4865   cint 4907   ciun 4954   ciin 4955  dom cdm 5633  ran crn 5634   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  Fincfn 8883  t crest 17302  Topctop 22242  Clsdccld 22367  clsccl 22369  Hauscha 22659  Compccmp 22737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9347  df-rest 17304  df-topgen 17325  df-top 22243  df-topon 22260  df-bases 22296  df-cld 22370  df-cls 22372  df-haus 22666  df-cmp 22738
This theorem is referenced by:  hauscmp  22758  hausllycmp  22845
  Copyright terms: Public domain W3C validator