Metamath Proof Explorer

Theorem hauscmplem

Description: Lemma for hauscmp . (Contributed by Mario Carneiro, 27-Nov-2013)

Ref Expression
Hypotheses hauscmp.1 ⊢ 𝑋 = ∪ 𝐽
hauscmplem.2 ⊢ 𝑂 = { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) }
hauscmplem.3 ⊢ ( 𝜑 → 𝐽 ∈ Haus )
hauscmplem.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
hauscmplem.5 ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ Comp )
hauscmplem.6 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 ∖ 𝑆 ) )
Assertion hauscmplem ( 𝜑 → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 hauscmp.1 ⊢ 𝑋 = ∪ 𝐽
2 hauscmplem.2 ⊢ 𝑂 = { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) }
3 hauscmplem.3 ⊢ ( 𝜑 → 𝐽 ∈ Haus )
4 hauscmplem.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
5 hauscmplem.5 ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ Comp )
6 hauscmplem.6 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 ∖ 𝑆 ) )
7 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
8 3 7 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
9 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝐽 ∈ Top )
10 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
11 9 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝑋 ∈ 𝐽 )
12 6 eldifad ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
13 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝐴 ∈ 𝑋 )
14 1 clstop ⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
15 9 14 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
16 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝑆 ⊆ ∪ 𝑥 )
17 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
18 uni0 ⊢ ∪ ∅ = ∅
19 17 18 eqtrdi ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∅ )
20 19 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ∪ 𝑥 = ∅ )
21 16 20 sseqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝑆 ⊆ ∅ )
22 ss0 ⊢ ( 𝑆 ⊆ ∅ → 𝑆 = ∅ )
23 21 22 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → 𝑆 = ∅ )
24 23 difeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ( 𝑋 ∖ 𝑆 ) = ( 𝑋 ∖ ∅ ) )
25 dif0 ⊢ ( 𝑋 ∖ ∅ ) = 𝑋
26 24 25 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ( 𝑋 ∖ 𝑆 ) = 𝑋 )
27 15 26 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = ( 𝑋 ∖ 𝑆 ) )
28 eqimss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = ( 𝑋 ∖ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
29 27 28 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
30 eleq2 ⊢ ( 𝑧 = 𝑋 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋 ) )
31 fveq2 ⊢ ( 𝑧 = 𝑋 → ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) )
32 31 sseq1d ⊢ ( 𝑧 = 𝑋 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
33 30 32 anbi12d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
34 33 rspcev ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
35 11 13 29 34 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 = ∅ ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
36 elin ⊢ ( 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ↔ ( 𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin ) )
37 id ⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ Fin )
38 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂 )
39 38 sseld ⊢ ( 𝑥 ∈ 𝒫 𝑂 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂 ) )
40 difeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑧 ) )
41 40 sseq2d ⊢ ( 𝑦 = 𝑧 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) )
42 41 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
43 42 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ↔ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
44 43 2 elrab2 ⊢ ( 𝑧 ∈ 𝑂 ↔ ( 𝑧 ∈ 𝐽 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
45 44 simprbi ⊢ ( 𝑧 ∈ 𝑂 → ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) )
46 39 45 syl6 ⊢ ( 𝑥 ∈ 𝒫 𝑂 → ( 𝑧 ∈ 𝑥 → ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
47 46 ralrimiv ⊢ ( 𝑥 ∈ 𝒫 𝑂 → ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) )
48 eleq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ) )
49 fveq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
50 49 sseq1d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) )
51 48 50 anbi12d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ↔ ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
52 51 ac6sfi ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
53 37 47 52 syl2anr ⊢ ( ( 𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
54 36 53 sylbi ⊢ ( 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) → ∃ 𝑓 ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
55 54 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) → ∃ 𝑓 ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) )
56 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝐽 ∈ Top )
57 frn ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → ran 𝑓 ⊆ 𝐽 )
58 57 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ran 𝑓 ⊆ 𝐽 )
59 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ≠ ∅ )
60 simpl ⊢ ( ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) → 𝑓 : 𝑥 ⟶ 𝐽 )
61 fdm ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → dom 𝑓 = 𝑥 )
62 61 eqeq1d ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → ( dom 𝑓 = ∅ ↔ 𝑥 = ∅ ) )
63 dm0rn0 ⊢ ( dom 𝑓 = ∅ ↔ ran 𝑓 = ∅ )
64 62 63 bitr3di ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → ( 𝑥 = ∅ ↔ ran 𝑓 = ∅ ) )
65 64 necon3bid ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → ( 𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅ ) )
66 65 biimpac ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) → ran 𝑓 ≠ ∅ )
67 59 60 66 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ran 𝑓 ≠ ∅ )
68 36 simprbi ⊢ ( 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) → 𝑥 ∈ Fin )
69 68 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ Fin )
70 ffn ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → 𝑓 Fn 𝑥 )
71 dffn4 ⊢ ( 𝑓 Fn 𝑥 ↔ 𝑓 : 𝑥 –onto→ ran 𝑓 )
72 70 71 sylib ⊢ ( 𝑓 : 𝑥 ⟶ 𝐽 → 𝑓 : 𝑥 –onto→ ran 𝑓 )
73 72 adantr ⊢ ( ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) → 𝑓 : 𝑥 –onto→ ran 𝑓 )
74 fofi ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑓 : 𝑥 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
75 69 73 74 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ran 𝑓 ∈ Fin )
76 fiinopn ⊢ ( 𝐽 ∈ Top → ( ( ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin ) → ∩ ran 𝑓 ∈ 𝐽 ) )
77 76 imp ⊢ ( ( 𝐽 ∈ Top ∧ ( ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin ) ) → ∩ ran 𝑓 ∈ 𝐽 )
78 56 58 67 75 77 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ ran 𝑓 ∈ 𝐽 )
79 simpl ⊢ ( ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) )
80 79 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → ∀ 𝑧 ∈ 𝑥 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) )
81 80 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝑥 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) )
82 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝐴 ∈ ( 𝑋 ∖ 𝑆 ) )
83 eliin ⊢ ( 𝐴 ∈ ( 𝑋 ∖ 𝑆 ) → ( 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ) )
84 82 83 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ( 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ) )
85 81 84 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) )
86 70 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝑓 Fn 𝑥 )
87 fnrnfv ⊢ ( 𝑓 Fn 𝑥 → ran 𝑓 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝑥 𝑦 = ( 𝑓 ‘ 𝑧 ) } )
88 87 inteqd ⊢ ( 𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑥 𝑦 = ( 𝑓 ‘ 𝑧 ) } )
89 fvex ⊢ ( 𝑓 ‘ 𝑧 ) ∈ V
90 89 dfiin2 ⊢ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) = ∩ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑥 𝑦 = ( 𝑓 ‘ 𝑧 ) }
91 88 90 eqtr4di ⊢ ( 𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) )
92 86 91 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) )
93 85 92 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝐴 ∈ ∩ ran 𝑓 )
94 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝑥 ≠ ∅ )
95 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → 𝐽 ∈ Top )
96 ffvelrn ⊢ ( ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝐽 )
97 96 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝐽 )
98 elssuni ⊢ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝐽 → ( 𝑓 ‘ 𝑧 ) ⊆ ∪ 𝐽 )
99 97 98 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ⊆ ∪ 𝐽 )
100 99 1 sseqtrrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ⊆ 𝑋 )
101 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑓 ‘ 𝑧 ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
102 95 100 101 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
103 102 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) → ∀ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
104 103 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
105 iincld ⊢ ( ( 𝑥 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
106 94 104 105 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) )
107 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑓 ‘ 𝑧 ) ⊆ 𝑋 ) → ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
108 95 100 107 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
109 108 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) → ∀ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
110 ssel ⊢ ( ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑧 ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ) )
111 110 ral2imi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → ( ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑓 ‘ 𝑧 ) → ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ) )
112 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑓 ‘ 𝑧 ) ) )
113 112 elv ⊢ ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑓 ‘ 𝑧 ) )
114 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ) )
115 114 elv ⊢ ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
116 111 113 115 3imtr4g ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ) )
117 116 ssrdv ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
118 109 117 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑓 : 𝑥 ⟶ 𝐽 ) → ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
119 118 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( 𝑓 ‘ 𝑧 ) ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
120 92 119 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
121 1 clsss2 ⊢ ( ( ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
122 106 120 121 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) )
123 ssel ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ) )
124 123 adantl ⊢ ( ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ) )
125 124 ral2imi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → ( ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ) )
126 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ) )
127 126 elv ⊢ ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) )
128 125 115 127 3imtr4g ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → ( 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) ) )
129 128 ssrdv ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) → ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) )
130 129 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) )
131 iindif2 ⊢ ( 𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) = ( 𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧 ) )
132 94 131 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) = ( 𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧 ) )
133 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → 𝑆 ⊆ ∪ 𝑥 )
134 uniiun ⊢ ∪ 𝑥 = ∪ 𝑧 ∈ 𝑥 𝑧
135 134 sseq2i ⊢ ( 𝑆 ⊆ ∪ 𝑥 ↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 )
136 sscon ⊢ ( 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → ( 𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
137 135 136 sylbi ⊢ ( 𝑆 ⊆ ∪ 𝑥 → ( 𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
138 133 137 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ( 𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
139 132 138 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
140 130 139 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∩ 𝑧 ∈ 𝑥 ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑆 ) )
141 122 140 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
142 eleq2 ⊢ ( 𝑧 = ∩ ran 𝑓 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran 𝑓 ) )
143 fveq2 ⊢ ( 𝑧 = ∩ ran 𝑓 → ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) = ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) )
144 143 sseq1d ⊢ ( 𝑧 = ∩ ran 𝑓 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
145 142 144 anbi12d ⊢ ( 𝑧 = ∩ ran 𝑓 → ( ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ↔ ( 𝐴 ∈ ∩ ran 𝑓 ∧ ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
146 145 rspcev ⊢ ( ( ∩ ran 𝑓 ∈ 𝐽 ∧ ( 𝐴 ∈ ∩ ran 𝑓 ∧ ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑓 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
147 78 93 141 146 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑓 : 𝑥 ⟶ 𝐽 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝐴 ∈ ( 𝑓 ‘ 𝑧 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑓 ‘ 𝑧 ) ) ⊆ ( 𝑋 ∖ 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
148 55 147 exlimddv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅ ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
149 148 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
150 35 149 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) ) ∧ 𝑆 ⊆ ∪ 𝑥 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
151 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ Haus )
152 4 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
153 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
154 id ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆 )
155 6 eldifbd ⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝑆 )
156 nelne2 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆 ) → 𝑥 ≠ 𝐴 )
157 154 155 156 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≠ 𝐴 )
158 1 hausnei ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) )
159 151 152 153 157 158 syl13anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) )
160 3anass ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) ) )
161 elssuni ⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽 )
162 161 1 sseqtrrdi ⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋 )
163 162 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → 𝑤 ⊆ 𝑋 )
164 incom ⊢ ( 𝑦 ∩ 𝑤 ) = ( 𝑤 ∩ 𝑦 )
165 164 eqeq1i ⊢ ( ( 𝑦 ∩ 𝑤 ) = ∅ ↔ ( 𝑤 ∩ 𝑦 ) = ∅ )
166 reldisj ⊢ ( 𝑤 ⊆ 𝑋 → ( ( 𝑤 ∩ 𝑦 ) = ∅ ↔ 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) ) )
167 165 166 syl5bb ⊢ ( 𝑤 ⊆ 𝑋 → ( ( 𝑦 ∩ 𝑤 ) = ∅ ↔ 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) ) )
168 163 167 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝑦 ∩ 𝑤 ) = ∅ ↔ 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) ) )
169 151 7 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ Top )
170 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
171 169 170 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
172 171 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
173 1 clsss2 ⊢ ( ( ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) )
174 173 ex ⊢ ( ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) → ( 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) )
175 172 174 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝑤 ⊆ ( 𝑋 ∖ 𝑦 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) )
176 168 175 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝑦 ∩ 𝑤 ) = ∅ → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) )
177 176 anim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) → ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) )
178 177 anim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) ) → ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ) )
179 160 178 syl5bi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) → ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ) )
180 179 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) → ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ) )
181 r19.42v ⊢ ( ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) )
182 180 181 syl6ib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) → ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ) )
183 182 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∃ 𝑦 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ ( 𝑦 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) ) )
184 159 183 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) )
185 2 unieqi ⊢ ∪ 𝑂 = ∪ { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) }
186 185 eleq2i ⊢ ( 𝑥 ∈ ∪ 𝑂 ↔ 𝑥 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) } )
187 elunirab ⊢ ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) } ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) )
188 186 187 bitri ⊢ ( 𝑥 ∈ ∪ 𝑂 ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑤 ∈ 𝐽 ( 𝐴 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) ) )
189 184 188 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ∪ 𝑂 )
190 189 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂 ) )
191 190 ssrdv ⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝑂 )
192 unieq ⊢ ( 𝑧 = 𝑂 → ∪ 𝑧 = ∪ 𝑂 )
193 192 sseq2d ⊢ ( 𝑧 = 𝑂 → ( 𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂 ) )
194 pweq ⊢ ( 𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂 )
195 194 ineq1d ⊢ ( 𝑧 = 𝑂 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑂 ∩ Fin ) )
196 195 rexeqdv ⊢ ( 𝑧 = 𝑂 → ( ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ↔ ∃ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) )
197 193 196 imbi12d ⊢ ( 𝑧 = 𝑂 → ( ( 𝑆 ⊆ ∪ 𝑧 → ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) ↔ ( 𝑆 ⊆ ∪ 𝑂 → ∃ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) ) )
198 1 cmpsub ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑧 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑧 → ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) ) )
199 198 biimp3a ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ∀ 𝑧 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑧 → ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) )
200 8 4 5 199 syl3anc ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑧 → ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) )
201 2 ssrab3 ⊢ 𝑂 ⊆ 𝐽
202 elpw2g ⊢ ( 𝐽 ∈ Haus → ( 𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽 ) )
203 3 202 syl ⊢ ( 𝜑 → ( 𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽 ) )
204 201 203 mpbiri ⊢ ( 𝜑 → 𝑂 ∈ 𝒫 𝐽 )
205 197 200 204 rspcdva ⊢ ( 𝜑 → ( 𝑆 ⊆ ∪ 𝑂 → ∃ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 ) )
206 191 205 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑂 ∩ Fin ) 𝑆 ⊆ ∪ 𝑥 )
207 150 206 r19.29a ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )