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

Theorem hauscmplem 21489
Description: Lemma for hauscmp 21490. (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 21415 . . . . . . 7 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
43ad3antrrr 721 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5 hauscmp.1 . . . . . 6 𝑋 = 𝐽
65topopn 20990 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
74, 6syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑋𝐽)
8 hauscmplem.6 . . . . . 6 (𝜑𝐴 ∈ (𝑋𝑆))
98eldifad 3744 . . . . 5 (𝜑𝐴𝑋)
109ad3antrrr 721 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐴𝑋)
115clstop 21153 . . . . . . 7 (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
124, 11syl 17 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13 simplr 785 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 𝑥)
14 unieq 4602 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
15 uni0 4623 . . . . . . . . . . . 12 ∅ = ∅
1614, 15syl6eq 2815 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1716adantl 473 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑥 = ∅)
1813, 17sseqtrd 3801 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19 ss0 4136 . . . . . . . . 9 (𝑆 ⊆ ∅ → 𝑆 = ∅)
2018, 19syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
2120difeq2d 3890 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = (𝑋 ∖ ∅))
22 dif0 4115 . . . . . . 7 (𝑋 ∖ ∅) = 𝑋
2321, 22syl6eq 2815 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = 𝑋)
2412, 23eqtr4d 2802 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋𝑆))
25 eqimss 3817 . . . . 5 (((cls‘𝐽)‘𝑋) = (𝑋𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
2624, 25syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
27 eleq2 2833 . . . . . 6 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
28 fveq2 6375 . . . . . . 7 (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
2928sseq1d 3792 . . . . . 6 (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆)))
3027, 29anbi12d 624 . . . . 5 (𝑧 = 𝑋 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))))
3130rspcev 3461 . . . 4 ((𝑋𝐽 ∧ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
327, 10, 26, 31syl12anc 865 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
33 elin 3958 . . . . . . 7 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin))
34 id 22 . . . . . . . 8 (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35 elpwi 4325 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑂𝑥𝑂)
3635sseld 3760 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥𝑧𝑂))
37 difeq2 3884 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑋𝑦) = (𝑋𝑧))
3837sseq2d 3793 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
3938anbi2d 622 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4039rexbidv 3199 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
41 hauscmplem.2 . . . . . . . . . . . 12 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
4240, 41elrab2 3523 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑧𝐽 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4342simprbi 490 . . . . . . . . . 10 (𝑧𝑂 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
4436, 43syl6 35 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4544ralrimiv 3112 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑂 → ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
46 eleq2 2833 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (𝐴𝑤𝐴 ∈ (𝑓𝑧)))
47 fveq2 6375 . . . . . . . . . . 11 (𝑤 = (𝑓𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓𝑧)))
4847sseq1d 3792 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧) ↔ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))
4946, 48anbi12d 624 . . . . . . . . 9 (𝑤 = (𝑓𝑧) → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)) ↔ (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5049ac6sfi 8411 . . . . . . . 8 ((𝑥 ∈ Fin ∧ ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5134, 45, 50syl2anr 590 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5233, 51sylbi 208 . . . . . 6 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5352ad2antlr 718 . . . . 5 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
543ad3antrrr 721 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐽 ∈ Top)
55 frn 6229 . . . . . . . 8 (𝑓:𝑥𝐽 → ran 𝑓𝐽)
5655ad2antrl 719 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
57 simprr 789 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58 simpl 474 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥𝐽)
59 dm0rn0 5510 . . . . . . . . . . 11 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
60 fdm 6231 . . . . . . . . . . . 12 (𝑓:𝑥𝐽 → dom 𝑓 = 𝑥)
6160eqeq1d 2767 . . . . . . . . . . 11 (𝑓:𝑥𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
6259, 61syl5rbbr 277 . . . . . . . . . 10 (𝑓:𝑥𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
6362necon3bid 2981 . . . . . . . . 9 (𝑓:𝑥𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
6463biimpac 470 . . . . . . . 8 ((𝑥 ≠ ∅ ∧ 𝑓:𝑥𝐽) → ran 𝑓 ≠ ∅)
6557, 58, 64syl2an 589 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ≠ ∅)
6633simprbi 490 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
6766ad2antlr 718 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68 ffn 6223 . . . . . . . . . 10 (𝑓:𝑥𝐽𝑓 Fn 𝑥)
69 dffn4 6304 . . . . . . . . . 10 (𝑓 Fn 𝑥𝑓:𝑥onto→ran 𝑓)
7068, 69sylib 209 . . . . . . . . 9 (𝑓:𝑥𝐽𝑓:𝑥onto→ran 𝑓)
7170adantr 472 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥onto→ran 𝑓)
72 fofi 8459 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝑓:𝑥onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7367, 71, 72syl2an 589 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ∈ Fin)
74 fiinopn 20985 . . . . . . . 8 (𝐽 ∈ Top → ((ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝐽))
7574imp 395 . . . . . . 7 ((𝐽 ∈ Top ∧ (ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝐽)
7654, 56, 65, 73, 75syl13anc 1491 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
77 simpl 474 . . . . . . . . . 10 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝐴 ∈ (𝑓𝑧))
7877ralimi 3099 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
7978ad2antll 720 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
808ad3antrrr 721 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ∈ (𝑋𝑆))
81 eliin 4681 . . . . . . . . 9 (𝐴 ∈ (𝑋𝑆) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8280, 81syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8379, 82mpbird 248 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 𝑧𝑥 (𝑓𝑧))
8468ad2antrl 719 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑓 Fn 𝑥)
85 fnrnfv 6431 . . . . . . . . . 10 (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
8685inteqd 4638 . . . . . . . . 9 (𝑓 Fn 𝑥 ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
87 fvex 6388 . . . . . . . . . 10 (𝑓𝑧) ∈ V
8887dfiin2 4711 . . . . . . . . 9 𝑧𝑥 (𝑓𝑧) = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)}
8986, 88syl6eqr 2817 . . . . . . . 8 (𝑓 Fn 𝑥 ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9084, 89syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9183, 90eleqtrrd 2847 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ran 𝑓)
9257adantr 472 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑥 ≠ ∅)
933ad4antr 724 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → 𝐽 ∈ Top)
94 ffvelrn 6547 . . . . . . . . . . . . . . 15 ((𝑓:𝑥𝐽𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
9594adantll 705 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
96 elssuni 4625 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝐽 → (𝑓𝑧) ⊆ 𝐽)
9795, 96syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝐽)
9897, 5syl6sseqr 3812 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝑋)
995clscld 21131 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10093, 98, 99syl2anc 579 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
101100ralrimiva 3113 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
102101adantrr 708 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
103 iincld 21123 . . . . . . . . 9 ((𝑥 ≠ ∅ ∧ ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10492, 102, 103syl2anc 579 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
1055sscls 21140 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
10693, 98, 105syl2anc 579 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
107106ralrimiva 3113 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
108 ssel 3755 . . . . . . . . . . . . . 14 ((𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 ∈ (𝑓𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
109108ral2imi 3094 . . . . . . . . . . . . 13 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (∀𝑧𝑥 𝑦 ∈ (𝑓𝑧) → ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
110 vex 3353 . . . . . . . . . . . . . 14 𝑦 ∈ V
111 eliin 4681 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧)))
112110, 111ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧))
113 eliin 4681 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
114110, 113ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)))
115109, 112, 1143imtr4g 287 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 𝑧𝑥 (𝑓𝑧) → 𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))))
116115ssrdv 3767 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
117107, 116syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
118117adantrr 708 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
11990, 118eqsstrd 3799 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
1205clsss2 21156 . . . . . . . 8 (( 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽) ∧ ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
121104, 119, 120syl2anc 579 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
122 ssel 3755 . . . . . . . . . . . . 13 (((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
123122adantl 473 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
124123ral2imi 3094 . . . . . . . . . . 11 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
125 eliin 4681 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
126110, 125ax-mp 5 . . . . . . . . . . 11 (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧))
127124, 114, 1263imtr4g 287 . . . . . . . . . 10 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 𝑧𝑥 (𝑋𝑧)))
128127ssrdv 3767 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
129128ad2antll 720 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
130 iindif2 4745 . . . . . . . . . 10 (𝑥 ≠ ∅ → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
13192, 130syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
132 simplrl 795 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑆 𝑥)
133 uniiun 4729 . . . . . . . . . . . 12 𝑥 = 𝑧𝑥 𝑧
134133sseq2i 3790 . . . . . . . . . . 11 (𝑆 𝑥𝑆 𝑧𝑥 𝑧)
135 sscon 3906 . . . . . . . . . . 11 (𝑆 𝑧𝑥 𝑧 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
136134, 135sylbi 208 . . . . . . . . . 10 (𝑆 𝑥 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
137132, 136syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
138131, 137eqsstrd 3799 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) ⊆ (𝑋𝑆))
139129, 138sstrd 3771 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑆))
140121, 139sstrd 3771 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))
141 eleq2 2833 . . . . . . . 8 (𝑧 = ran 𝑓 → (𝐴𝑧𝐴 ran 𝑓))
142 fveq2 6375 . . . . . . . . 9 (𝑧 = ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘ ran 𝑓))
143142sseq1d 3792 . . . . . . . 8 (𝑧 = ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆)))
144141, 143anbi12d 624 . . . . . . 7 (𝑧 = ran 𝑓 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))))
145144rspcev 3461 . . . . . 6 (( ran 𝑓𝐽 ∧ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14676, 91, 140, 145syl12anc 865 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14753, 146exlimddv 2030 . . . 4 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
148147anassrs 459 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14932, 148pm2.61dane 3024 . 2 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
1501adantr 472 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐽 ∈ Haus)
151 hauscmplem.4 . . . . . . . . 9 (𝜑𝑆𝑋)
152151sselda 3761 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝑋)
1539adantr 472 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴𝑋)
154 id 22 . . . . . . . . 9 (𝑥𝑆𝑥𝑆)
1558eldifbd 3745 . . . . . . . . 9 (𝜑 → ¬ 𝐴𝑆)
156 nelne2 3034 . . . . . . . . 9 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
157154, 155, 156syl2anr 590 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝐴)
1585hausnei 21412 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥𝑋𝐴𝑋𝑥𝐴)) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
159150, 152, 153, 157, 158syl13anc 1491 . . . . . . 7 ((𝜑𝑥𝑆) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
160 3anass 1116 . . . . . . . . . . 11 ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) ↔ (𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)))
161 elssuni 4625 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤 𝐽)
162161, 5syl6sseqr 3812 . . . . . . . . . . . . . . . 16 (𝑤𝐽𝑤𝑋)
163162adantl 473 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → 𝑤𝑋)
164 incom 3967 . . . . . . . . . . . . . . . . 17 (𝑦𝑤) = (𝑤𝑦)
165164eqeq1i 2770 . . . . . . . . . . . . . . . 16 ((𝑦𝑤) = ∅ ↔ (𝑤𝑦) = ∅)
166 reldisj 4181 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑤𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
167165, 166syl5bb 274 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
168163, 167syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
169150, 2syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐽 ∈ Top)
1705opncld 21117 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
171169, 170sylan 575 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
172171adantr 472 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
1735clsss2 21156 . . . . . . . . . . . . . . . 16 (((𝑋𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))
174173ex 401 . . . . . . . . . . . . . . 15 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
175172, 174syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
176168, 175sylbid 231 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
177176anim2d 605 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
178177anim2d 605 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
179160, 178syl5bi 233 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
180179reximdva 3163 . . . . . . . . 9 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
181 r19.42v 3239 . . . . . . . . 9 (∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))) ↔ (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
182180, 181syl6ib 242 . . . . . . . 8 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
183182reximdva 3163 . . . . . . 7 ((𝜑𝑥𝑆) → (∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
184159, 183mpd 15 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
18541unieqi 4603 . . . . . . . 8 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
186185eleq2i 2836 . . . . . . 7 (𝑥 𝑂𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))})
187 elunirab 4606 . . . . . . 7 (𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
188186, 187bitri 266 . . . . . 6 (𝑥 𝑂 ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
189184, 188sylibr 225 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 𝑂)
190189ex 401 . . . 4 (𝜑 → (𝑥𝑆𝑥 𝑂))
191190ssrdv 3767 . . 3 (𝜑𝑆 𝑂)
192 unieq 4602 . . . . . 6 (𝑧 = 𝑂 𝑧 = 𝑂)
193192sseq2d 3793 . . . . 5 (𝑧 = 𝑂 → (𝑆 𝑧𝑆 𝑂))
194 pweq 4318 . . . . . . 7 (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
195194ineq1d 3975 . . . . . 6 (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
196195rexeqdv 3293 . . . . 5 (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
197193, 196imbi12d 335 . . . 4 (𝑧 = 𝑂 → ((𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥) ↔ (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)))
198 hauscmplem.5 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
1995cmpsub 21483 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)))
200199biimp3a 1593 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ (𝐽t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
2013, 151, 198, 200syl3anc 1490 . . . 4 (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
202 ssrab2 3847 . . . . . 6 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ⊆ 𝐽
20341, 202eqsstri 3795 . . . . 5 𝑂𝐽
204 elpw2g 4985 . . . . . 6 (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
2051, 204syl 17 . . . . 5 (𝜑 → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
206203, 205mpbiri 249 . . . 4 (𝜑𝑂 ∈ 𝒫 𝐽)
207197, 201, 206rspcdva 3467 . . 3 (𝜑 → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
208191, 207mpd 15 . 2 (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)
209149, 208r19.29a 3225 1 (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   cuni 4594   cint 4633   ciun 4676   ciin 4677  dom cdm 5277  ran crn 5278   Fn wfn 6063  wf 6064  ontowfo 6066  cfv 6068  (class class class)co 6842  Fincfn 8160  t crest 16349  Topctop 20977  Clsdccld 21100  clsccl 21102  Hauscha 21392  Compccmp 21469
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 2069  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 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
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 2062  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 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-fin 8164  df-fi 8524  df-rest 16351  df-topgen 16372  df-top 20978  df-topon 20995  df-bases 21030  df-cld 21103  df-cls 21105  df-haus 21399  df-cmp 21470
This theorem is referenced by:  hauscmp  21490  hausllycmp  21577
  Copyright terms: Public domain W3C validator