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

Theorem hauscmplem 21119
Description: Lemma for hauscmp 21120. (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 21045 . . . . . . 7 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
43ad3antrrr 765 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5 hauscmp.1 . . . . . 6 𝑋 = 𝐽
65topopn 20636 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
74, 6syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑋𝐽)
8 hauscmplem.6 . . . . . 6 (𝜑𝐴 ∈ (𝑋𝑆))
98eldifad 3567 . . . . 5 (𝜑𝐴𝑋)
109ad3antrrr 765 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐴𝑋)
115clstop 20783 . . . . . . 7 (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
124, 11syl 17 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13 simplr 791 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 𝑥)
14 unieq 4410 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
15 uni0 4431 . . . . . . . . . . . 12 ∅ = ∅
1614, 15syl6eq 2671 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1716adantl 482 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑥 = ∅)
1813, 17sseqtrd 3620 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19 ss0 3946 . . . . . . . . 9 (𝑆 ⊆ ∅ → 𝑆 = ∅)
2018, 19syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
2120difeq2d 3706 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = (𝑋 ∖ ∅))
22 dif0 3924 . . . . . . 7 (𝑋 ∖ ∅) = 𝑋
2321, 22syl6eq 2671 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = 𝑋)
2412, 23eqtr4d 2658 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋𝑆))
25 eqimss 3636 . . . . 5 (((cls‘𝐽)‘𝑋) = (𝑋𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
2624, 25syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
27 eleq2 2687 . . . . . 6 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
28 fveq2 6148 . . . . . . 7 (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
2928sseq1d 3611 . . . . . 6 (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆)))
3027, 29anbi12d 746 . . . . 5 (𝑧 = 𝑋 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))))
3130rspcev 3295 . . . 4 ((𝑋𝐽 ∧ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
327, 10, 26, 31syl12anc 1321 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
33 elin 3774 . . . . . . 7 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin))
34 id 22 . . . . . . . 8 (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35 elpwi 4140 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑂𝑥𝑂)
3635sseld 3582 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥𝑧𝑂))
37 difeq2 3700 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑋𝑦) = (𝑋𝑧))
3837sseq2d 3612 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
3938anbi2d 739 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4039rexbidv 3045 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
41 hauscmplem.2 . . . . . . . . . . . 12 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
4240, 41elrab2 3348 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑧𝐽 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4342simprbi 480 . . . . . . . . . 10 (𝑧𝑂 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
4436, 43syl6 35 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4544ralrimiv 2959 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑂 → ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
46 eleq2 2687 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (𝐴𝑤𝐴 ∈ (𝑓𝑧)))
47 fveq2 6148 . . . . . . . . . . 11 (𝑤 = (𝑓𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓𝑧)))
4847sseq1d 3611 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧) ↔ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))
4946, 48anbi12d 746 . . . . . . . . 9 (𝑤 = (𝑓𝑧) → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)) ↔ (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5049ac6sfi 8148 . . . . . . . 8 ((𝑥 ∈ Fin ∧ ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5134, 45, 50syl2anr 495 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5233, 51sylbi 207 . . . . . 6 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5352ad2antlr 762 . . . . 5 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
543ad3antrrr 765 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐽 ∈ Top)
55 frn 6010 . . . . . . . 8 (𝑓:𝑥𝐽 → ran 𝑓𝐽)
5655ad2antrl 763 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
57 simprr 795 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58 simpl 473 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥𝐽)
59 dm0rn0 5302 . . . . . . . . . . 11 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
60 fdm 6008 . . . . . . . . . . . 12 (𝑓:𝑥𝐽 → dom 𝑓 = 𝑥)
6160eqeq1d 2623 . . . . . . . . . . 11 (𝑓:𝑥𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
6259, 61syl5rbbr 275 . . . . . . . . . 10 (𝑓:𝑥𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
6362necon3bid 2834 . . . . . . . . 9 (𝑓:𝑥𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
6463biimpac 503 . . . . . . . 8 ((𝑥 ≠ ∅ ∧ 𝑓:𝑥𝐽) → ran 𝑓 ≠ ∅)
6557, 58, 64syl2an 494 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ≠ ∅)
6633simprbi 480 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
6766ad2antlr 762 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68 ffn 6002 . . . . . . . . . 10 (𝑓:𝑥𝐽𝑓 Fn 𝑥)
69 dffn4 6078 . . . . . . . . . 10 (𝑓 Fn 𝑥𝑓:𝑥onto→ran 𝑓)
7068, 69sylib 208 . . . . . . . . 9 (𝑓:𝑥𝐽𝑓:𝑥onto→ran 𝑓)
7170adantr 481 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥onto→ran 𝑓)
72 fofi 8196 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝑓:𝑥onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7367, 71, 72syl2an 494 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ∈ Fin)
74 fiinopn 20631 . . . . . . . 8 (𝐽 ∈ Top → ((ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝐽))
7574imp 445 . . . . . . 7 ((𝐽 ∈ Top ∧ (ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝐽)
7654, 56, 65, 73, 75syl13anc 1325 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
77 simpl 473 . . . . . . . . . 10 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝐴 ∈ (𝑓𝑧))
7877ralimi 2947 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
7978ad2antll 764 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
808ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ∈ (𝑋𝑆))
81 eliin 4491 . . . . . . . . 9 (𝐴 ∈ (𝑋𝑆) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8280, 81syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8379, 82mpbird 247 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 𝑧𝑥 (𝑓𝑧))
8468ad2antrl 763 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑓 Fn 𝑥)
85 fnrnfv 6199 . . . . . . . . . 10 (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
8685inteqd 4445 . . . . . . . . 9 (𝑓 Fn 𝑥 ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
87 fvex 6158 . . . . . . . . . 10 (𝑓𝑧) ∈ V
8887dfiin2 4521 . . . . . . . . 9 𝑧𝑥 (𝑓𝑧) = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)}
8986, 88syl6eqr 2673 . . . . . . . 8 (𝑓 Fn 𝑥 ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9084, 89syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9183, 90eleqtrrd 2701 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ran 𝑓)
9257adantr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑥 ≠ ∅)
933ad4antr 767 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → 𝐽 ∈ Top)
94 ffvelrn 6313 . . . . . . . . . . . . . . 15 ((𝑓:𝑥𝐽𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
9594adantll 749 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
96 elssuni 4433 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝐽 → (𝑓𝑧) ⊆ 𝐽)
9795, 96syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝐽)
9897, 5syl6sseqr 3631 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝑋)
995clscld 20761 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10093, 98, 99syl2anc 692 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
101100ralrimiva 2960 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
102101adantrr 752 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
103 iincld 20753 . . . . . . . . 9 ((𝑥 ≠ ∅ ∧ ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10492, 102, 103syl2anc 692 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
1055sscls 20770 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
10693, 98, 105syl2anc 692 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
107106ralrimiva 2960 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
108 ssel 3577 . . . . . . . . . . . . . 14 ((𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 ∈ (𝑓𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
109108ral2imi 2942 . . . . . . . . . . . . 13 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (∀𝑧𝑥 𝑦 ∈ (𝑓𝑧) → ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
110 vex 3189 . . . . . . . . . . . . . 14 𝑦 ∈ V
111 eliin 4491 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧)))
112110, 111ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧))
113 eliin 4491 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
114110, 113ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)))
115109, 112, 1143imtr4g 285 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 𝑧𝑥 (𝑓𝑧) → 𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))))
116115ssrdv 3589 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
117107, 116syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
118117adantrr 752 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
11990, 118eqsstrd 3618 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
1205clsss2 20786 . . . . . . . 8 (( 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽) ∧ ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
121104, 119, 120syl2anc 692 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
122 ssel 3577 . . . . . . . . . . . . 13 (((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
123122adantl 482 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
124123ral2imi 2942 . . . . . . . . . . 11 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
125 eliin 4491 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
126110, 125ax-mp 5 . . . . . . . . . . 11 (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧))
127124, 114, 1263imtr4g 285 . . . . . . . . . 10 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 𝑧𝑥 (𝑋𝑧)))
128127ssrdv 3589 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
129128ad2antll 764 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
130 iindif2 4555 . . . . . . . . . 10 (𝑥 ≠ ∅ → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
13192, 130syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
132 simplrl 799 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑆 𝑥)
133 uniiun 4539 . . . . . . . . . . . 12 𝑥 = 𝑧𝑥 𝑧
134133sseq2i 3609 . . . . . . . . . . 11 (𝑆 𝑥𝑆 𝑧𝑥 𝑧)
135 sscon 3722 . . . . . . . . . . 11 (𝑆 𝑧𝑥 𝑧 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
136134, 135sylbi 207 . . . . . . . . . 10 (𝑆 𝑥 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
137132, 136syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
138131, 137eqsstrd 3618 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) ⊆ (𝑋𝑆))
139129, 138sstrd 3593 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑆))
140121, 139sstrd 3593 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))
141 eleq2 2687 . . . . . . . 8 (𝑧 = ran 𝑓 → (𝐴𝑧𝐴 ran 𝑓))
142 fveq2 6148 . . . . . . . . 9 (𝑧 = ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘ ran 𝑓))
143142sseq1d 3611 . . . . . . . 8 (𝑧 = ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆)))
144141, 143anbi12d 746 . . . . . . 7 (𝑧 = ran 𝑓 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))))
145144rspcev 3295 . . . . . 6 (( ran 𝑓𝐽 ∧ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14676, 91, 140, 145syl12anc 1321 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14753, 146exlimddv 1860 . . . 4 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
148147anassrs 679 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14932, 148pm2.61dane 2877 . 2 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
1501adantr 481 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐽 ∈ Haus)
151 hauscmplem.4 . . . . . . . . 9 (𝜑𝑆𝑋)
152151sselda 3583 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝑋)
1539adantr 481 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴𝑋)
154 id 22 . . . . . . . . 9 (𝑥𝑆𝑥𝑆)
1558eldifbd 3568 . . . . . . . . 9 (𝜑 → ¬ 𝐴𝑆)
156 nelne2 2887 . . . . . . . . 9 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
157154, 155, 156syl2anr 495 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝐴)
1585hausnei 21042 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥𝑋𝐴𝑋𝑥𝐴)) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
159150, 152, 153, 157, 158syl13anc 1325 . . . . . . 7 ((𝜑𝑥𝑆) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
160 3anass 1040 . . . . . . . . . . 11 ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) ↔ (𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)))
161 elssuni 4433 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤 𝐽)
162161, 5syl6sseqr 3631 . . . . . . . . . . . . . . . 16 (𝑤𝐽𝑤𝑋)
163162adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → 𝑤𝑋)
164 incom 3783 . . . . . . . . . . . . . . . . 17 (𝑦𝑤) = (𝑤𝑦)
165164eqeq1i 2626 . . . . . . . . . . . . . . . 16 ((𝑦𝑤) = ∅ ↔ (𝑤𝑦) = ∅)
166 reldisj 3992 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑤𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
167165, 166syl5bb 272 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
168163, 167syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
169150, 2syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐽 ∈ Top)
1705opncld 20747 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
171169, 170sylan 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
172171adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
1735clsss2 20786 . . . . . . . . . . . . . . . 16 (((𝑋𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))
174173ex 450 . . . . . . . . . . . . . . 15 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
175172, 174syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
176168, 175sylbid 230 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
177176anim2d 588 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
178177anim2d 588 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
179160, 178syl5bi 232 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
180179reximdva 3011 . . . . . . . . 9 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
181 r19.42v 3084 . . . . . . . . 9 (∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))) ↔ (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
182180, 181syl6ib 241 . . . . . . . 8 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
183182reximdva 3011 . . . . . . 7 ((𝜑𝑥𝑆) → (∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
184159, 183mpd 15 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
18541unieqi 4411 . . . . . . . 8 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
186185eleq2i 2690 . . . . . . 7 (𝑥 𝑂𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))})
187 elunirab 4414 . . . . . . 7 (𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
188186, 187bitri 264 . . . . . 6 (𝑥 𝑂 ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
189184, 188sylibr 224 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 𝑂)
190189ex 450 . . . 4 (𝜑 → (𝑥𝑆𝑥 𝑂))
191190ssrdv 3589 . . 3 (𝜑𝑆 𝑂)
192 ssrab2 3666 . . . . . 6 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ⊆ 𝐽
19341, 192eqsstri 3614 . . . . 5 𝑂𝐽
194 elpw2g 4787 . . . . . 6 (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
1951, 194syl 17 . . . . 5 (𝜑 → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
196193, 195mpbiri 248 . . . 4 (𝜑𝑂 ∈ 𝒫 𝐽)
197 hauscmplem.5 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
1985cmpsub 21113 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)))
199198biimp3a 1429 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ (𝐽t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
2003, 151, 197, 199syl3anc 1323 . . . 4 (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
201 unieq 4410 . . . . . . 7 (𝑧 = 𝑂 𝑧 = 𝑂)
202201sseq2d 3612 . . . . . 6 (𝑧 = 𝑂 → (𝑆 𝑧𝑆 𝑂))
203 pweq 4133 . . . . . . . 8 (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
204203ineq1d 3791 . . . . . . 7 (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
205204rexeqdv 3134 . . . . . 6 (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
206202, 205imbi12d 334 . . . . 5 (𝑧 = 𝑂 → ((𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥) ↔ (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)))
207206rspcva 3293 . . . 4 ((𝑂 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)) → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
208196, 200, 207syl2anc 692 . . 3 (𝜑 → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
209191, 208mpd 15 . 2 (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)
210149, 209r19.29a 3071 1 (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cdif 3552  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130   cuni 4402   cint 4440   ciun 4485   ciin 4486  dom cdm 5074  ran crn 5075   Fn wfn 5842  wf 5843  ontowfo 5845  cfv 5847  (class class class)co 6604  Fincfn 7899  t crest 16002  Topctop 20617  Clsdccld 20730  clsccl 20732  Hauscha 21022  Compccmp 21099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-top 20621  df-bases 20622  df-topon 20623  df-cld 20733  df-cls 20735  df-haus 21029  df-cmp 21100
This theorem is referenced by:  hauscmp  21120  hausllycmp  21207
  Copyright terms: Public domain W3C validator