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→ 𝒫 𝒫 𝐴 )