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

Theorem hauscmplem 21019
 Description: Lemma for hauscmp 21020. (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 20945 . . . . . . 7 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
43ad3antrrr 762 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5 hauscmp.1 . . . . . 6 𝑋 = 𝐽
65topopn 20536 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
74, 6syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑋𝐽)
8 hauscmplem.6 . . . . . 6 (𝜑𝐴 ∈ (𝑋𝑆))
98eldifad 3552 . . . . 5 (𝜑𝐴𝑋)
109ad3antrrr 762 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝐴𝑋)
115clstop 20683 . . . . . . 7 (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
124, 11syl 17 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13 simplr 788 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 𝑥)
14 unieq 4380 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
15 uni0 4401 . . . . . . . . . . . 12 ∅ = ∅
1614, 15syl6eq 2660 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1716adantl 481 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑥 = ∅)
1813, 17sseqtrd 3604 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19 ss0 3926 . . . . . . . . 9 (𝑆 ⊆ ∅ → 𝑆 = ∅)
2018, 19syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
2120difeq2d 3690 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = (𝑋 ∖ ∅))
22 dif0 3904 . . . . . . 7 (𝑋 ∖ ∅) = 𝑋
2321, 22syl6eq 2660 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → (𝑋𝑆) = 𝑋)
2412, 23eqtr4d 2647 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋𝑆))
25 eqimss 3620 . . . . 5 (((cls‘𝐽)‘𝑋) = (𝑋𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
2624, 25syl 17 . . . 4 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))
27 eleq2 2677 . . . . . 6 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
28 fveq2 6103 . . . . . . 7 (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
2928sseq1d 3595 . . . . . 6 (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆)))
3027, 29anbi12d 743 . . . . 5 (𝑧 = 𝑋 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))))
3130rspcev 3282 . . . 4 ((𝑋𝐽 ∧ (𝐴𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
327, 10, 26, 31syl12anc 1316 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 = ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
33 elin 3758 . . . . . . 7 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin))
34 id 22 . . . . . . . 8 (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35 elpwi 4117 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑂𝑥𝑂)
3635sseld 3567 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥𝑧𝑂))
37 difeq2 3684 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑋𝑦) = (𝑋𝑧))
3837sseq2d 3596 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
3938anbi2d 736 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4039rexbidv 3034 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)) ↔ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
41 hauscmplem.2 . . . . . . . . . . . 12 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
4240, 41elrab2 3333 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑧𝐽 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4342simprbi 479 . . . . . . . . . 10 (𝑧𝑂 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
4436, 43syl6 34 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑂 → (𝑧𝑥 → ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))))
4544ralrimiv 2948 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑂 → ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)))
46 eleq2 2677 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (𝐴𝑤𝐴 ∈ (𝑓𝑧)))
47 fveq2 6103 . . . . . . . . . . 11 (𝑤 = (𝑓𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓𝑧)))
4847sseq1d 3595 . . . . . . . . . 10 (𝑤 = (𝑓𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧) ↔ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))
4946, 48anbi12d 743 . . . . . . . . 9 (𝑤 = (𝑓𝑧) → ((𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧)) ↔ (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5049ac6sfi 8089 . . . . . . . 8 ((𝑥 ∈ Fin ∧ ∀𝑧𝑥𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑧))) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5134, 45, 50syl2anr 494 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑂𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5233, 51sylbi 206 . . . . . 6 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
5352ad2antlr 759 . . . . 5 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))))
543ad3antrrr 762 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐽 ∈ Top)
55 frn 5966 . . . . . . . 8 (𝑓:𝑥𝐽 → ran 𝑓𝐽)
5655ad2antrl 760 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
57 simprr 792 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58 simpl 472 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥𝐽)
59 dm0rn0 5263 . . . . . . . . . . 11 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
60 fdm 5964 . . . . . . . . . . . 12 (𝑓:𝑥𝐽 → dom 𝑓 = 𝑥)
6160eqeq1d 2612 . . . . . . . . . . 11 (𝑓:𝑥𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
6259, 61syl5rbbr 274 . . . . . . . . . 10 (𝑓:𝑥𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
6362necon3bid 2826 . . . . . . . . 9 (𝑓:𝑥𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
6463biimpac 502 . . . . . . . 8 ((𝑥 ≠ ∅ ∧ 𝑓:𝑥𝐽) → ran 𝑓 ≠ ∅)
6557, 58, 64syl2an 493 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ≠ ∅)
6633simprbi 479 . . . . . . . . 9 (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
6766ad2antlr 759 . . . . . . . 8 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68 ffn 5958 . . . . . . . . . 10 (𝑓:𝑥𝐽𝑓 Fn 𝑥)
69 dffn4 6034 . . . . . . . . . 10 (𝑓 Fn 𝑥𝑓:𝑥onto→ran 𝑓)
7068, 69sylib 207 . . . . . . . . 9 (𝑓:𝑥𝐽𝑓:𝑥onto→ran 𝑓)
7170adantr 480 . . . . . . . 8 ((𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧))) → 𝑓:𝑥onto→ran 𝑓)
72 fofi 8135 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝑓:𝑥onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7367, 71, 72syl2an 493 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 ∈ Fin)
74 fiinopn 20531 . . . . . . . 8 (𝐽 ∈ Top → ((ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ran 𝑓𝐽))
7574imp 444 . . . . . . 7 ((𝐽 ∈ Top ∧ (ran 𝑓𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ran 𝑓𝐽)
7654, 56, 65, 73, 75syl13anc 1320 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓𝐽)
77 simpl 472 . . . . . . . . . 10 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝐴 ∈ (𝑓𝑧))
7877ralimi 2936 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
7978ad2antll 761 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧))
808ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ∈ (𝑋𝑆))
81 eliin 4461 . . . . . . . . 9 (𝐴 ∈ (𝑋𝑆) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8280, 81syl 17 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝐴 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝐴 ∈ (𝑓𝑧)))
8379, 82mpbird 246 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 𝑧𝑥 (𝑓𝑧))
8468ad2antrl 760 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑓 Fn 𝑥)
85 fnrnfv 6152 . . . . . . . . . 10 (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
8685inteqd 4415 . . . . . . . . 9 (𝑓 Fn 𝑥 ran 𝑓 = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)})
87 fvex 6113 . . . . . . . . . 10 (𝑓𝑧) ∈ V
8887dfiin2 4491 . . . . . . . . 9 𝑧𝑥 (𝑓𝑧) = {𝑦 ∣ ∃𝑧𝑥 𝑦 = (𝑓𝑧)}
8986, 88syl6eqr 2662 . . . . . . . 8 (𝑓 Fn 𝑥 ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9084, 89syl 17 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 = 𝑧𝑥 (𝑓𝑧))
9183, 90eleqtrrd 2691 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝐴 ran 𝑓)
9257adantr 480 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑥 ≠ ∅)
933ad4antr 764 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → 𝐽 ∈ Top)
94 ffvelrn 6265 . . . . . . . . . . . . . . 15 ((𝑓:𝑥𝐽𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
9594adantll 746 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ 𝐽)
96 elssuni 4403 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝐽 → (𝑓𝑧) ⊆ 𝐽)
9795, 96syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝐽)
9897, 5syl6sseqr 3615 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ 𝑋)
995clscld 20661 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10093, 98, 99syl2anc 691 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
101100ralrimiva 2949 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
102101adantrr 749 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
103 iincld 20653 . . . . . . . . 9 ((𝑥 ≠ ∅ ∧ ∀𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
10492, 102, 103syl2anc 691 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽))
1055sscls 20670 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ (𝑓𝑧) ⊆ 𝑋) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
10693, 98, 105syl2anc 691 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) ∧ 𝑧𝑥) → (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
107106ralrimiva 2949 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → ∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)))
108 ssel 3562 . . . . . . . . . . . . . 14 ((𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 ∈ (𝑓𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
109108ral2imi 2931 . . . . . . . . . . . . 13 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (∀𝑧𝑥 𝑦 ∈ (𝑓𝑧) → ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
110 vex 3176 . . . . . . . . . . . . . 14 𝑦 ∈ V
111 eliin 4461 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧)))
112110, 111ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 (𝑓𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑓𝑧))
113 eliin 4461 . . . . . . . . . . . . . 14 (𝑦 ∈ V → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧))))
114110, 113ax-mp 5 . . . . . . . . . . . . 13 (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ↔ ∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)))
115109, 112, 1143imtr4g 284 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → (𝑦 𝑧𝑥 (𝑓𝑧) → 𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))))
116115ssrdv 3574 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑓𝑧) ⊆ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
117107, 116syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ 𝑓:𝑥𝐽) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
118117adantrr 749 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑓𝑧) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
11990, 118eqsstrd 3602 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
1205clsss2 20686 . . . . . . . 8 (( 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ∈ (Clsd‘𝐽) ∧ ran 𝑓 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
121104, 119, 120syl2anc 691 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)))
122 ssel 3562 . . . . . . . . . . . . 13 (((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
123122adantl 481 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 ∈ (𝑋𝑧)))
124123ral2imi 2931 . . . . . . . . . . 11 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (∀𝑧𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓𝑧)) → ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
125 eliin 4461 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧)))
126110, 125ax-mp 5 . . . . . . . . . . 11 (𝑦 𝑧𝑥 (𝑋𝑧) ↔ ∀𝑧𝑥 𝑦 ∈ (𝑋𝑧))
127124, 114, 1263imtr4g 284 . . . . . . . . . 10 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → (𝑦 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) → 𝑦 𝑧𝑥 (𝑋𝑧)))
128127ssrdv 3574 . . . . . . . . 9 (∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
129128ad2antll 761 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ 𝑧𝑥 (𝑋𝑧))
130 iindif2 4525 . . . . . . . . . 10 (𝑥 ≠ ∅ → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
13192, 130syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) = (𝑋 𝑧𝑥 𝑧))
132 simplrl 796 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑆 𝑥)
133 uniiun 4509 . . . . . . . . . . . 12 𝑥 = 𝑧𝑥 𝑧
134133sseq2i 3593 . . . . . . . . . . 11 (𝑆 𝑥𝑆 𝑧𝑥 𝑧)
135 sscon 3706 . . . . . . . . . . 11 (𝑆 𝑧𝑥 𝑧 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
136134, 135sylbi 206 . . . . . . . . . 10 (𝑆 𝑥 → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
137132, 136syl 17 . . . . . . . . 9 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → (𝑋 𝑧𝑥 𝑧) ⊆ (𝑋𝑆))
138131, 137eqsstrd 3602 . . . . . . . 8 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 (𝑋𝑧) ⊆ (𝑋𝑆))
139129, 138sstrd 3578 . . . . . . 7 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → 𝑧𝑥 ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑆))
140121, 139sstrd 3578 . . . . . 6 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))
141 eleq2 2677 . . . . . . . 8 (𝑧 = ran 𝑓 → (𝐴𝑧𝐴 ran 𝑓))
142 fveq2 6103 . . . . . . . . 9 (𝑧 = ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘ ran 𝑓))
143142sseq1d 3595 . . . . . . . 8 (𝑧 = ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆) ↔ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆)))
144141, 143anbi12d 743 . . . . . . 7 (𝑧 = ran 𝑓 → ((𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)) ↔ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))))
145144rspcev 3282 . . . . . 6 (( ran 𝑓𝐽 ∧ (𝐴 ran 𝑓 ∧ ((cls‘𝐽)‘ ran 𝑓) ⊆ (𝑋𝑆))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14676, 91, 140, 145syl12anc 1316 . . . . 5 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) ∧ (𝑓:𝑥𝐽 ∧ ∀𝑧𝑥 (𝐴 ∈ (𝑓𝑧) ∧ ((cls‘𝐽)‘(𝑓𝑧)) ⊆ (𝑋𝑧)))) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14753, 146exlimddv 1850 . . . 4 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 𝑥𝑥 ≠ ∅)) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
148147anassrs 678 . . 3 ((((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
14932, 148pm2.61dane 2869 . 2 (((𝜑𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 𝑥) → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
1501adantr 480 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐽 ∈ Haus)
151 hauscmplem.4 . . . . . . . . 9 (𝜑𝑆𝑋)
152151sselda 3568 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝑋)
1539adantr 480 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴𝑋)
154 id 22 . . . . . . . . 9 (𝑥𝑆𝑥𝑆)
1558eldifbd 3553 . . . . . . . . 9 (𝜑 → ¬ 𝐴𝑆)
156 nelne2 2879 . . . . . . . . 9 ((𝑥𝑆 ∧ ¬ 𝐴𝑆) → 𝑥𝐴)
157154, 155, 156syl2anr 494 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝑥𝐴)
1585hausnei 20942 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥𝑋𝐴𝑋𝑥𝐴)) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
159150, 152, 153, 157, 158syl13anc 1320 . . . . . . 7 ((𝜑𝑥𝑆) → ∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅))
160 3anass 1035 . . . . . . . . . . 11 ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) ↔ (𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)))
161 elssuni 4403 . . . . . . . . . . . . . . . . 17 (𝑤𝐽𝑤 𝐽)
162161, 5syl6sseqr 3615 . . . . . . . . . . . . . . . 16 (𝑤𝐽𝑤𝑋)
163162adantl 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → 𝑤𝑋)
164 incom 3767 . . . . . . . . . . . . . . . . 17 (𝑦𝑤) = (𝑤𝑦)
165164eqeq1i 2615 . . . . . . . . . . . . . . . 16 ((𝑦𝑤) = ∅ ↔ (𝑤𝑦) = ∅)
166 reldisj 3972 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑤𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
167165, 166syl5bb 271 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
168163, 167syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋𝑦)))
169150, 2syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐽 ∈ Top)
1705opncld 20647 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
171169, 170sylan 487 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
172171adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
1735clsss2 20686 . . . . . . . . . . . . . . . 16 (((𝑋𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))
174173ex 449 . . . . . . . . . . . . . . 15 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
175172, 174syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → (𝑤 ⊆ (𝑋𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
176168, 175sylbid 229 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑦𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))
177176anim2d 587 . . . . . . . . . . . 12 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
178177anim2d 587 . . . . . . . . . . 11 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦 ∧ (𝐴𝑤 ∧ (𝑦𝑤) = ∅)) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
179160, 178syl5bi 231 . . . . . . . . . 10 ((((𝜑𝑥𝑆) ∧ 𝑦𝐽) ∧ 𝑤𝐽) → ((𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
180179reximdva 3000 . . . . . . . . 9 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
181 r19.42v 3073 . . . . . . . . 9 (∃𝑤𝐽 (𝑥𝑦 ∧ (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))) ↔ (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
182180, 181syl6ib 240 . . . . . . . 8 (((𝜑𝑥𝑆) ∧ 𝑦𝐽) → (∃𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
183182reximdva 3000 . . . . . . 7 ((𝜑𝑥𝑆) → (∃𝑦𝐽𝑤𝐽 (𝑥𝑦𝐴𝑤 ∧ (𝑦𝑤) = ∅) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦)))))
184159, 183mpd 15 . . . . . 6 ((𝜑𝑥𝑆) → ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
18541unieqi 4381 . . . . . . . 8 𝑂 = {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))}
186185eleq2i 2680 . . . . . . 7 (𝑥 𝑂𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))})
187 elunirab 4384 . . . . . . 7 (𝑥 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
188186, 187bitri 263 . . . . . 6 (𝑥 𝑂 ↔ ∃𝑦𝐽 (𝑥𝑦 ∧ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))))
189184, 188sylibr 223 . . . . 5 ((𝜑𝑥𝑆) → 𝑥 𝑂)
190189ex 449 . . . 4 (𝜑 → (𝑥𝑆𝑥 𝑂))
191190ssrdv 3574 . . 3 (𝜑𝑆 𝑂)
192 ssrab2 3650 . . . . . 6 {𝑦𝐽 ∣ ∃𝑤𝐽 (𝐴𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋𝑦))} ⊆ 𝐽
19341, 192eqsstri 3598 . . . . 5 𝑂𝐽
194 elpw2g 4754 . . . . . 6 (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
1951, 194syl 17 . . . . 5 (𝜑 → (𝑂 ∈ 𝒫 𝐽𝑂𝐽))
196193, 195mpbiri 247 . . . 4 (𝜑𝑂 ∈ 𝒫 𝐽)
197 hauscmplem.5 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ Comp)
1985cmpsub 21013 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)))
199198biimp3a 1424 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ (𝐽t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
2003, 151, 197, 199syl3anc 1318 . . . 4 (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥))
201 unieq 4380 . . . . . . 7 (𝑧 = 𝑂 𝑧 = 𝑂)
202201sseq2d 3596 . . . . . 6 (𝑧 = 𝑂 → (𝑆 𝑧𝑆 𝑂))
203 pweq 4111 . . . . . . . 8 (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
204203ineq1d 3775 . . . . . . 7 (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
205204rexeqdv 3122 . . . . . 6 (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
206202, 205imbi12d 333 . . . . 5 (𝑧 = 𝑂 → ((𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥) ↔ (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)))
207206rspcva 3280 . . . 4 ((𝑂 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝒫 𝐽(𝑆 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 𝑥)) → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
208196, 200, 207syl2anc 691 . . 3 (𝜑 → (𝑆 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥))
209191, 208mpd 15 . 2 (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 𝑥)
210149, 209r19.29a 3060 1 (𝜑 → ∃𝑧𝐽 (𝐴𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋𝑆)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455  ∩ ciin 4456  dom cdm 5038  ran crn 5039   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549  Fincfn 7841   ↾t crest 15904  Topctop 20517  Clsdccld 20630  clsccl 20632  Hauscha 20922  Compccmp 20999 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-cls 20635  df-haus 20929  df-cmp 21000 This theorem is referenced by:  hauscmp  21020  hausllycmp  21107
 Copyright terms: Public domain W3C validator