Metamath Proof Explorer

Theorem hauspwpwf1

Description: Lemma for hauspwpwdom . Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015)

Ref Expression
Hypotheses hauspwpwf1.x ⊢ 𝑋 = ∪ 𝐽
hauspwpwf1.f ⊢ 𝐹 = ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
Assertion hauspwpwf1 ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 )

Proof

Step Hyp Ref Expression
1 hauspwpwf1.x ⊢ 𝑋 = ∪ 𝐽
2 hauspwpwf1.f ⊢ 𝐹 = ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
3 inss2 ⊢ ( 𝑗 ∩ 𝐴 ) ⊆ 𝐴
4 vex ⊢ 𝑗 ∈ V
5 4 inex1 ⊢ ( 𝑗 ∩ 𝐴 ) ∈ V
6 5 elpw ⊢ ( ( 𝑗 ∩ 𝐴 ) ∈ 𝒫 𝐴 ↔ ( 𝑗 ∩ 𝐴 ) ⊆ 𝐴 )
7 3 6 mpbir ⊢ ( 𝑗 ∩ 𝐴 ) ∈ 𝒫 𝐴
8 eleq1 ⊢ ( 𝑎 = ( 𝑗 ∩ 𝐴 ) → ( 𝑎 ∈ 𝒫 𝐴 ↔ ( 𝑗 ∩ 𝐴 ) ∈ 𝒫 𝐴 ) )
9 7 8 mpbiri ⊢ ( 𝑎 = ( 𝑗 ∩ 𝐴 ) → 𝑎 ∈ 𝒫 𝐴 )
10 9 adantl ⊢ ( ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) → 𝑎 ∈ 𝒫 𝐴 )
11 10 rexlimivw ⊢ ( ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) → 𝑎 ∈ 𝒫 𝐴 )
12 11 abssi ⊢ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ⊆ 𝒫 𝐴
13 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
14 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
15 13 14 syl ⊢ ( 𝐽 ∈ Haus → 𝑋 ∈ 𝐽 )
16 ssexg ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝐴 ∈ V )
17 15 16 sylan2 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐽 ∈ Haus ) → 𝐴 ∈ V )
18 17 ancoms ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
19 pwexg ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
20 elpw2g ⊢ ( 𝒫 𝐴 ∈ V → ( { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ⊆ 𝒫 𝐴 ) )
21 18 19 20 3syl ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ⊆ 𝒫 𝐴 ) )
22 12 21 mpbiri ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ∈ 𝒫 𝒫 𝐴 )
23 22 a1d ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ∈ 𝒫 𝒫 𝐴 ) )
24 simplll ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐽 ∈ Haus )
25 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
26 13 25 sylan ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
27 26 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
28 simplrl ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
29 27 28 sseldd ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝑋 )
30 simplrr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
31 27 30 sseldd ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝑋 )
32 simpr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
33 1 hausnei ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑘 ∈ 𝐽 ∃ 𝑙 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) )
34 24 29 31 32 33 syl13anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑘 ∈ 𝐽 ∃ 𝑙 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) )
35 simprll ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → 𝑘 ∈ 𝐽 )
36 simprr1 ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → 𝑥 ∈ 𝑘 )
37 eqidd ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → ( 𝑘 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) )
38 elequ2 ⊢ ( 𝑗 = 𝑘 → ( 𝑥 ∈ 𝑗 ↔ 𝑥 ∈ 𝑘 ) )
39 ineq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) )
40 39 eqeq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ↔ ( 𝑘 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) ) )
41 38 40 anbi12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑘 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) ) ) )
42 41 rspcev ⊢ ( ( 𝑘 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) ) ) → ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
43 35 36 37 42 syl12anc ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
44 vex ⊢ 𝑘 ∈ V
45 44 inex1 ⊢ ( 𝑘 ∩ 𝐴 ) ∈ V
46 eqeq1 ⊢ ( 𝑎 = ( 𝑘 ∩ 𝐴 ) → ( 𝑎 = ( 𝑗 ∩ 𝐴 ) ↔ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
47 46 anbi2d ⊢ ( 𝑎 = ( 𝑘 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ) )
48 47 rexbidv ⊢ ( 𝑎 = ( 𝑘 ∩ 𝐴 ) → ( ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ) )
49 45 48 elab ⊢ ( ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ↔ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
50 43 49 sylibr ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
51 13 ad2antrr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ Top )
52 51 ad3antrrr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝐽 ∈ Top )
53 simplr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝑋 )
54 53 ad3antrrr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝐴 ⊆ 𝑋 )
55 simprr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
56 55 ad3antrrr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
57 simplr ⊢ ( ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) → 𝑙 ∈ 𝐽 )
58 57 ad2antlr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑙 ∈ 𝐽 )
59 simprl ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑗 ∈ 𝐽 )
60 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑙 ∈ 𝐽 ∧ 𝑗 ∈ 𝐽 ) → ( 𝑙 ∩ 𝑗 ) ∈ 𝐽 )
61 52 58 59 60 syl3anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ( 𝑙 ∩ 𝑗 ) ∈ 𝐽 )
62 simpr2 ⊢ ( ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) → 𝑦 ∈ 𝑙 )
63 62 ad2antlr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑦 ∈ 𝑙 )
64 simprr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑦 ∈ 𝑗 )
65 63 64 elind ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → 𝑦 ∈ ( 𝑙 ∩ 𝑗 ) )
66 1 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( ( 𝑙 ∩ 𝑗 ) ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑙 ∩ 𝑗 ) ) ) → ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) ≠ ∅ )
67 52 54 56 61 65 66 syl32anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) ≠ ∅ )
68 n0 ⊢ ( ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) )
69 67 68 sylib ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ∃ 𝑧 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) )
70 elin ⊢ ( 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) ↔ ( 𝑧 ∈ ( 𝑙 ∩ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) )
71 elin ⊢ ( 𝑧 ∈ ( 𝑙 ∩ 𝑗 ) ↔ ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) )
72 71 anbi1i ⊢ ( ( 𝑧 ∈ ( 𝑙 ∩ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ↔ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) )
73 70 72 bitri ⊢ ( 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) ↔ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) )
74 elin ⊢ ( 𝑧 ∈ ( 𝑗 ∩ 𝐴 ) ↔ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ∈ 𝐴 ) )
75 74 biimpri ⊢ ( ( 𝑧 ∈ 𝑗 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝑗 ∩ 𝐴 ) )
76 75 adantll ⊢ ( ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝑗 ∩ 𝐴 ) )
77 76 ad2antll ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → 𝑧 ∈ ( 𝑗 ∩ 𝐴 ) )
78 simpll ⊢ ( ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝑙 )
79 78 ad2antll ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → 𝑧 ∈ 𝑙 )
80 simpr3 ⊢ ( ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) → ( 𝑘 ∩ 𝑙 ) = ∅ )
81 80 ad2antlr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → ( 𝑘 ∩ 𝑙 ) = ∅ )
82 minel ⊢ ( ( 𝑧 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) → ¬ 𝑧 ∈ 𝑘 )
83 elinel1 ⊢ ( 𝑧 ∈ ( 𝑘 ∩ 𝐴 ) → 𝑧 ∈ 𝑘 )
84 82 83 nsyl ⊢ ( ( 𝑧 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) → ¬ 𝑧 ∈ ( 𝑘 ∩ 𝐴 ) )
85 79 81 84 syl2anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → ¬ 𝑧 ∈ ( 𝑘 ∩ 𝐴 ) )
86 nelneq2 ⊢ ( ( 𝑧 ∈ ( 𝑗 ∩ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑘 ∩ 𝐴 ) ) → ¬ ( 𝑗 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) )
87 77 85 86 syl2anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → ¬ ( 𝑗 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) )
88 eqcom ⊢ ( ( 𝑗 ∩ 𝐴 ) = ( 𝑘 ∩ 𝐴 ) ↔ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) )
89 87 88 sylnib ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ∧ ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) ) ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) )
90 89 expr ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ( ( ( 𝑧 ∈ 𝑙 ∧ 𝑧 ∈ 𝑗 ) ∧ 𝑧 ∈ 𝐴 ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
91 73 90 syl5bi ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ( 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
92 91 exlimdv ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ( ∃ 𝑧 𝑧 ∈ ( ( 𝑙 ∩ 𝑗 ) ∩ 𝐴 ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
93 69 92 mpd ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ 𝑦 ∈ 𝑗 ) ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) )
94 93 anassrs ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ 𝑗 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑗 ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) )
95 nan ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ 𝑗 ∈ 𝐽 ) → ¬ ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ) ↔ ( ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ 𝑗 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑗 ) → ¬ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
96 94 95 mpbir ⊢ ( ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) ∧ 𝑗 ∈ 𝐽 ) → ¬ ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
97 96 nrexdv ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → ¬ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
98 46 anbi2d ⊢ ( 𝑎 = ( 𝑘 ∩ 𝐴 ) → ( ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ) )
99 98 rexbidv ⊢ ( 𝑎 = ( 𝑘 ∩ 𝐴 ) → ( ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) ) )
100 45 99 elab ⊢ ( ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ↔ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ ( 𝑘 ∩ 𝐴 ) = ( 𝑗 ∩ 𝐴 ) ) )
101 97 100 sylnibr ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → ¬ ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
102 nelne1 ⊢ ( ( ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ∧ ¬ ( 𝑘 ∩ 𝐴 ) ∈ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
103 50 101 102 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) ) ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
104 103 expr ⊢ ( ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑘 ∈ 𝐽 ∧ 𝑙 ∈ 𝐽 ) ) → ( ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) )
105 104 rexlimdvva ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ∃ 𝑘 ∈ 𝐽 ∃ 𝑙 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑙 ∧ ( 𝑘 ∩ 𝑙 ) = ∅ ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) )
106 34 105 mpd ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
107 106 ex ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ( 𝑥 ≠ 𝑦 → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ≠ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) )
108 107 necon4d ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ( { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } = { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } → 𝑥 = 𝑦 ) )
109 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑗 ↔ 𝑦 ∈ 𝑗 ) )
110 109 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ) )
111 110 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ↔ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) ) )
112 111 abbidv ⊢ ( 𝑥 = 𝑦 → { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } = { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } )
113 108 112 impbid1 ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ( { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } = { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ↔ 𝑥 = 𝑦 ) )
114 113 ex ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } = { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑦 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ↔ 𝑥 = 𝑦 ) ) )
115 23 114 dom2lem ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 )
116 f1eq1 ⊢ ( 𝐹 = ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) → ( 𝐹 : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 ) )
117 2 116 ax-mp ⊢ ( 𝐹 : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↦ { 𝑎 ∣ ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑗 ∧ 𝑎 = ( 𝑗 ∩ 𝐴 ) ) } ) : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 )
118 115 117 sylibr ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 : ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) –1-1→ 𝒫 𝒫 𝐴 )