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

Theorem hauscmplem 22014
Description: Lemma for hauscmp 22015. (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 21939 . . . . . . 7 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
43ad3antrrr 729 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5 hauscmp.1 . . . . . 6 𝑋 = 𝐽
65topopn 21514 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
74, 6syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑋𝐽)
8 hauscmplem.6 . . . . . 6 (𝜑𝐴 ∈ (𝑋𝑆))
98eldifad 3931 . . . . 5 (𝜑𝐴𝑋)
109ad3antrrr 729 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐴𝑋)
115clstop 21677 . . . . . . 7 (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
124, 11syl 17 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13 simplr 768 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 𝑥)
14 unieq 4835 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
15 uni0 4852 . . . . . . . . . . . 12 ∅ = ∅
1614, 15syl6eq 2875 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1716adantl 485 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑥 = ∅)
1813, 17sseqtrd 3993 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19 ss0 4335 . . . . . . . . 9 (𝑆 ⊆ ∅ → 𝑆 = ∅)
2018, 19syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
2120difeq2d 4085 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = (𝑋 ∖ ∅))
22 dif0 4315 . . . . . . 7 (𝑋 ∖ ∅) = 𝑋
2321, 22syl6eq 2875 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = 𝑋)
2412, 23eqtr4d 2862 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋𝑆))
25 eqimss 4009 . . . . 5 (((cls‘𝐽)‘𝑋) = (𝑋𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
2624, 25syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
27 eleq2 2904 . . . . . 6 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
28 fveq2 6661 . . . . . . 7 (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
2928sseq1d 3984 . . . . . 6 (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆)))
3027, 29anbi12d 633 . . . . 5 (𝑧 = 𝑋 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))))
3130rspcev 3609 . . . 4 ((𝑋𝐽 ∧ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
327, 10, 26, 31syl12anc 835 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
33 elin 3935 . . . . . . 7 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin))
34 id 22 . . . . . . . 8 (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35 elpwi 4531 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑂𝑥𝑂)
3635sseld 3952 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥𝑧𝑂))
37 difeq2 4079 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑋𝑦) = (𝑋𝑧))
3837sseq2d 3985 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
3938anbi2d 631 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4039rexbidv 3289 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
41 hauscmplem.2 . . . . . . . . . . . 12 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
4240, 41elrab2 3669 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑧𝐽 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4342simprbi 500 . . . . . . . . . 10 (𝑧𝑂 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
4436, 43syl6 35 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4544ralrimiv 3176 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑂 → ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
46 eleq2 2904 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (𝐴𝑤𝐴 ∈ (𝑓𝑧)))
47 fveq2 6661 . . . . . . . . . . 11 (𝑤 = (𝑓𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓𝑧)))
4847sseq1d 3984 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧) ↔ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))
4946, 48anbi12d 633 . . . . . . . . 9 (𝑤 = (𝑓𝑧) → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)) ↔ (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5049ac6sfi 8759 . . . . . . . 8 ((𝑥 ∈ Fin ∧ ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5134, 45, 50syl2anr 599 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5233, 51sylbi 220 . . . . . 6 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5352ad2antlr 726 . . . . 5 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
543ad3antrrr 729 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐽 ∈ Top)
55 frn 6509 . . . . . . . 8 (𝑓:𝑥𝐽 → ran 𝑓𝐽)
5655ad2antrl 727 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
57 simprr 772 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58 simpl 486 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥𝐽)
59 fdm 6511 . . . . . . . . . . . 12 (𝑓:𝑥𝐽 → dom 𝑓 = 𝑥)
6059eqeq1d 2826 . . . . . . . . . . 11 (𝑓:𝑥𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
61 dm0rn0 5782 . . . . . . . . . . 11 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
6260, 61bitr3di 289 . . . . . . . . . 10 (𝑓:𝑥𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
6362necon3bid 3058 . . . . . . . . 9 (𝑓:𝑥𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
6463biimpac 482 . . . . . . . 8 ((𝑥 ≠ ∅ ∧ 𝑓:𝑥𝐽) → ran 𝑓 ≠ ∅)
6557, 58, 64syl2an 598 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ≠ ∅)
6633simprbi 500 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
6766ad2antlr 726 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68 ffn 6503 . . . . . . . . . 10 (𝑓:𝑥𝐽𝑓 Fn 𝑥)
69 dffn4 6587 . . . . . . . . . 10 (𝑓 Fn 𝑥𝑓:𝑥onto→ran 𝑓)
7068, 69sylib 221 . . . . . . . . 9 (𝑓:𝑥𝐽𝑓:𝑥onto→ran 𝑓)
7170adantr 484 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥onto→ran 𝑓)
72 fofi 8807 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝑓:𝑥onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7367, 71, 72syl2an 598 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ∈ Fin)
74 fiinopn 21509 . . . . . . . 8 (𝐽 ∈ Top → ((ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝐽))
7574imp 410 . . . . . . 7 ((𝐽 ∈ Top ∧ (ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝐽)
7654, 56, 65, 73, 75syl13anc 1369 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
77 simpl 486 . . . . . . . . . 10 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝐴 ∈ (𝑓𝑧))
7877ralimi 3155 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
7978ad2antll 728 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
808ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ∈ (𝑋𝑆))
81 eliin 4910 . . . . . . . . 9 (𝐴 ∈ (𝑋𝑆) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8280, 81syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8379, 82mpbird 260 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 𝑧𝑥 (𝑓𝑧))
8468ad2antrl 727 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑓 Fn 𝑥)
85 fnrnfv 6716 . . . . . . . . . 10 (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
8685inteqd 4867 . . . . . . . . 9 (𝑓 Fn 𝑥 ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
87 fvex 6674 . . . . . . . . . 10 (𝑓𝑧) ∈ V
8887dfiin2 4945 . . . . . . . . 9 𝑧𝑥 (𝑓𝑧) = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)}
8986, 88syl6eqr 2877 . . . . . . . 8 (𝑓 Fn 𝑥 ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9084, 89syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9183, 90eleqtrrd 2919 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ran 𝑓)
9257adantr 484 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑥 ≠ ∅)
933ad4antr 731 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → 𝐽 ∈ Top)
94 ffvelrn 6840 . . . . . . . . . . . . . . 15 ((𝑓:𝑥𝐽𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
9594adantll 713 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
96 elssuni 4854 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝐽 → (𝑓𝑧) ⊆ 𝐽)
9795, 96syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝐽)
9897, 5sseqtrrdi 4004 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝑋)
995clscld 21655 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10093, 98, 99syl2anc 587 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
101100ralrimiva 3177 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
102101adantrr 716 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
103 iincld 21647 . . . . . . . . 9 ((𝑥 ≠ ∅ ∧ ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10492, 102, 103syl2anc 587 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
1055sscls 21664 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
10693, 98, 105syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
107106ralrimiva 3177 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
108 ssel 3946 . . . . . . . . . . . . . 14 ((𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 ∈ (𝑓𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
109108ral2imi 3151 . . . . . . . . . . . . 13 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (∀𝑧𝑥 𝑦 ∈ (𝑓𝑧) → ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
110 eliin 4910 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧)))
111110elv 3485 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧))
112 eliin 4910 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
113112elv 3485 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)))
114109, 111, 1133imtr4g 299 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 𝑧𝑥 (𝑓𝑧) → 𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))))
115114ssrdv 3959 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
116107, 115syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
117116adantrr 716 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
11890, 117eqsstrd 3991 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
1195clsss2 21680 . . . . . . . 8 (( 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽) ∧ ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
120104, 118, 119syl2anc 587 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
121 ssel 3946 . . . . . . . . . . . . 13 (((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
122121adantl 485 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
123122ral2imi 3151 . . . . . . . . . . 11 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
124 eliin 4910 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
125124elv 3485 . . . . . . . . . . 11 (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧))
126123, 113, 1253imtr4g 299 . . . . . . . . . 10 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 𝑧𝑥 (𝑋𝑧)))
127126ssrdv 3959 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
128127ad2antll 728 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
129 iindif2 4985 . . . . . . . . . 10 (𝑥 ≠ ∅ → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
13092, 129syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
131 simplrl 776 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑆 𝑥)
132 uniiun 4968 . . . . . . . . . . . 12 𝑥 = 𝑧𝑥 𝑧
133132sseq2i 3982 . . . . . . . . . . 11 (𝑆 𝑥𝑆 𝑧𝑥 𝑧)
134 sscon 4101 . . . . . . . . . . 11 (𝑆 𝑧𝑥 𝑧 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
135133, 134sylbi 220 . . . . . . . . . 10 (𝑆 𝑥 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
136131, 135syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
137130, 136eqsstrd 3991 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) ⊆ (𝑋𝑆))
138128, 137sstrd 3963 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑆))
139120, 138sstrd 3963 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))
140 eleq2 2904 . . . . . . . 8 (𝑧 = ran 𝑓 → (𝐴𝑧𝐴 ran 𝑓))
141 fveq2 6661 . . . . . . . . 9 (𝑧 = ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘ ran 𝑓))
142141sseq1d 3984 . . . . . . . 8 (𝑧 = ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆)))
143140, 142anbi12d 633 . . . . . . 7 (𝑧 = ran 𝑓 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))))
144143rspcev 3609 . . . . . 6 (( ran 𝑓𝐽 ∧ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14576, 91, 139, 144syl12anc 835 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14653, 145exlimddv 1937 . . . 4 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
147146anassrs 471 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14832, 147pm2.61dane 3101 . 2 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
1491adantr 484 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐽 ∈ Haus)
150 hauscmplem.4 . . . . . . . . 9 (𝜑𝑆𝑋)
151150sselda 3953 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝑋)
1529adantr 484 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴𝑋)
153 id 22 . . . . . . . . 9 (𝑥𝑆𝑥𝑆)
1548eldifbd 3932 . . . . . . . . 9 (𝜑 → ¬ 𝐴𝑆)
155 nelne2 3111 . . . . . . . . 9 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
156153, 154, 155syl2anr 599 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝐴)
1575hausnei 21936 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥𝑋𝐴𝑋𝑥𝐴)) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
158149, 151, 152, 156, 157syl13anc 1369 . . . . . . 7 ((𝜑𝑥𝑆) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
159 3anass 1092 . . . . . . . . . . 11 ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) ↔ (𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)))
160 elssuni 4854 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤 𝐽)
161160, 5sseqtrrdi 4004 . . . . . . . . . . . . . . . 16 (𝑤𝐽𝑤𝑋)
162161adantl 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → 𝑤𝑋)
163 incom 4163 . . . . . . . . . . . . . . . . 17 (𝑦𝑤) = (𝑤𝑦)
164163eqeq1i 2829 . . . . . . . . . . . . . . . 16 ((𝑦𝑤) = ∅ ↔ (𝑤𝑦) = ∅)
165 reldisj 4385 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑤𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
166164, 165syl5bb 286 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
167162, 166syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
168149, 2syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐽 ∈ Top)
1695opncld 21641 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
170168, 169sylan 583 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
171170adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
1725clsss2 21680 . . . . . . . . . . . . . . . 16 (((𝑋𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))
173172ex 416 . . . . . . . . . . . . . . 15 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
174171, 173syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
175167, 174sylbid 243 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
176175anim2d 614 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
177176anim2d 614 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
178159, 177syl5bi 245 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
179178reximdva 3266 . . . . . . . . 9 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
180 r19.42v 3341 . . . . . . . . 9 (∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))) ↔ (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
181179, 180syl6ib 254 . . . . . . . 8 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
182181reximdva 3266 . . . . . . 7 ((𝜑𝑥𝑆) → (∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
183158, 182mpd 15 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
18441unieqi 4837 . . . . . . . 8 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
185184eleq2i 2907 . . . . . . 7 (𝑥 𝑂𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))})
186 elunirab 4840 . . . . . . 7 (𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
187185, 186bitri 278 . . . . . 6 (𝑥 𝑂 ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
188183, 187sylibr 237 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 𝑂)
189188ex 416 . . . 4 (𝜑 → (𝑥𝑆𝑥 𝑂))
190189ssrdv 3959 . . 3 (𝜑𝑆 𝑂)
191 unieq 4835 . . . . . 6 (𝑧 = 𝑂 𝑧 = 𝑂)
192191sseq2d 3985 . . . . 5 (𝑧 = 𝑂 → (𝑆 𝑧𝑆 𝑂))
193 pweq 4538 . . . . . . 7 (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
194193ineq1d 4173 . . . . . 6 (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
195194rexeqdv 3403 . . . . 5 (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
196192, 195imbi12d 348 . . . 4 (𝑧 = 𝑂 → ((𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥) ↔ (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)))
197 hauscmplem.5 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
1985cmpsub 22008 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)))
199198biimp3a 1466 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ (𝐽t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
2003, 150, 197, 199syl3anc 1368 . . . 4 (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
20141ssrab3 4043 . . . . 5 𝑂𝐽
202 elpw2g 5233 . . . . . 6 (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
2031, 202syl 17 . . . . 5 (𝜑 → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
204201, 203mpbiri 261 . . . 4 (𝜑𝑂 ∈ 𝒫 𝐽)
205196, 200, 204rspcdva 3611 . . 3 (𝜑 → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
206190, 205mpd 15 . 2 (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)
207148, 206r19.29a 3281 1 (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2115  {cab 2802  wne 3014  wral 3133  wrex 3134  {crab 3137  Vcvv 3480  cdif 3916  cin 3918  wss 3919  c0 4276  𝒫 cpw 4522   cuni 4824   cint 4862   ciun 4905   ciin 4906  dom cdm 5542  ran crn 5543   Fn wfn 6338  wf 6339  ontowfo 6341  cfv 6343  (class class class)co 7149  Fincfn 8505  t crest 16694  Topctop 21501  Clsdccld 21624  clsccl 21626  Hauscha 21916  Compccmp 21994
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8285  df-en 8506  df-dom 8507  df-fin 8509  df-fi 8872  df-rest 16696  df-topgen 16717  df-top 21502  df-topon 21519  df-bases 21554  df-cld 21627  df-cls 21629  df-haus 21923  df-cmp 21995
This theorem is referenced by:  hauscmp  22015  hausllycmp  22102
  Copyright terms: Public domain W3C validator