This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfac14

Description: Theorem ptcls is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion dfac14 ( CHOICE ↔ ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
2 1 unieqd ⊢ ( 𝑘 = 𝑥 → ∪ ( 𝑓 ‘ 𝑘 ) = ∪ ( 𝑓 ‘ 𝑥 ) )
3 2 pweqd ⊢ ( 𝑘 = 𝑥 → 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) )
4 3 cbvixpv ⊢ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 )
5 4 eleq2i ⊢ ( 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ↔ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) )
6 simplr ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → 𝑓 : dom 𝑓 ⟶ Top )
7 6 feqmptd ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → 𝑓 = ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) )
8 7 fveq2d ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ( ∏t ‘ 𝑓 ) = ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) ) )
9 8 fveq2d ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ( cls ‘ ( ∏t ‘ 𝑓 ) ) = ( cls ‘ ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) ) ) )
10 9 fveq1d ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = ( ( cls ‘ ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) )
11 eqid ⊢ ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) ) = ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) )
12 vex ⊢ 𝑓 ∈ V
13 12 dmex ⊢ dom 𝑓 ∈ V
14 13 a1i ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → dom 𝑓 ∈ V )
15 6 ffvelcdmda ⊢ ( ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑘 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑘 ) ∈ Top )
16 toptopon2 ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ Top ↔ ( 𝑓 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝑓 ‘ 𝑘 ) ) )
17 15 16 sylib ⊢ ( ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑘 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝑓 ‘ 𝑘 ) ) )
18 simpr ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) )
19 18 5 sylibr ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) )
20 vex ⊢ 𝑠 ∈ V
21 20 elixp ⊢ ( 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ↔ ( 𝑠 Fn dom 𝑓 ∧ ∀ 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ∈ 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ) )
22 21 simprbi ⊢ ( 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) → ∀ 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ∈ 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) )
23 19 22 syl ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ∀ 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ∈ 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) )
24 23 r19.21bi ⊢ ( ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑘 ∈ dom 𝑓 ) → ( 𝑠 ‘ 𝑘 ) ∈ 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) )
25 24 elpwid ⊢ ( ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) ∧ 𝑘 ∈ dom 𝑓 ) → ( 𝑠 ‘ 𝑘 ) ⊆ ∪ ( 𝑓 ‘ 𝑘 ) )
26 fvex ⊢ ( 𝑠 ‘ 𝑘 ) ∈ V
27 13 26 iunex ⊢ ∪ 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ∈ V
28 simpll ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → CHOICE )
29 acacni ⊢ ( ( CHOICE ∧ dom 𝑓 ∈ V ) → AC dom 𝑓 = V )
30 28 13 29 sylancl ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → AC dom 𝑓 = V )
31 27 30 eleqtrrid ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ∪ 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ∈ AC dom 𝑓 )
32 11 14 17 25 31 ptclsg ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ( ( cls ‘ ( ∏t ‘ ( 𝑘 ∈ dom 𝑓 ↦ ( 𝑓 ‘ 𝑘 ) ) ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
33 10 32 eqtrd ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑥 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑥 ) ) → ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
34 5 33 sylan2b ⊢ ( ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) ∧ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ) → ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
35 34 ralrimiva ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Top ) → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
36 35 ex ⊢ ( CHOICE → ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
37 36 alrimiv ⊢ ( CHOICE → ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
38 vex ⊢ 𝑔 ∈ V
39 38 dmex ⊢ dom 𝑔 ∈ V
40 39 a1i ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → dom 𝑔 ∈ V )
41 fvex ⊢ ( 𝑔 ‘ 𝑥 ) ∈ V
42 41 a1i ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ∈ V )
43 simplrr ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ∅ ∉ ran 𝑔 )
44 df-nel ⊢ ( ∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔 )
45 43 44 sylib ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ¬ ∅ ∈ ran 𝑔 )
46 funforn ⊢ ( Fun 𝑔 ↔ 𝑔 : dom 𝑔 –onto→ ran 𝑔 )
47 fof ⊢ ( 𝑔 : dom 𝑔 –onto→ ran 𝑔 → 𝑔 : dom 𝑔 ⟶ ran 𝑔 )
48 46 47 sylbi ⊢ ( Fun 𝑔 → 𝑔 : dom 𝑔 ⟶ ran 𝑔 )
49 48 ad2antrl ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → 𝑔 : dom 𝑔 ⟶ ran 𝑔 )
50 49 ffvelcdmda ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
51 eleq1 ⊢ ( ( 𝑔 ‘ 𝑥 ) = ∅ → ( ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔 ) )
52 50 51 syl5ibcom ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ( ( 𝑔 ‘ 𝑥 ) = ∅ → ∅ ∈ ran 𝑔 ) )
53 52 necon3bd ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ( ¬ ∅ ∈ ran 𝑔 → ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
54 45 53 mpd ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
55 eqid ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) = 𝒫 ∪ ( 𝑔 ‘ 𝑥 )
56 eqid ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } = { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) }
57 eqid ⊢ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) = ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) )
58 fveq1 ⊢ ( 𝑠 = 𝑔 → ( 𝑠 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
59 58 ixpeq2dv ⊢ ( 𝑠 = 𝑔 → X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) = X 𝑘 ∈ dom 𝑔 ( 𝑔 ‘ 𝑘 ) )
60 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑥 ) )
61 60 cbvixpv ⊢ X 𝑘 ∈ dom 𝑔 ( 𝑔 ‘ 𝑘 ) = X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 )
62 59 61 eqtrdi ⊢ ( 𝑠 = 𝑔 → X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) = X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) )
63 62 fveq2d ⊢ ( 𝑠 = 𝑔 → ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ) )
64 58 fveq2d ⊢ ( 𝑠 = 𝑔 → ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) = ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑘 ) ) )
65 64 ixpeq2dv ⊢ ( 𝑠 = 𝑔 → X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑘 ) ) )
66 60 unieqd ⊢ ( 𝑘 = 𝑥 → ∪ ( 𝑔 ‘ 𝑘 ) = ∪ ( 𝑔 ‘ 𝑥 ) )
67 66 pweqd ⊢ ( 𝑘 = 𝑥 → 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) = 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) )
68 67 sneqd ⊢ ( 𝑘 = 𝑥 → { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } = { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } )
69 60 68 uneq12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) )
70 69 pweqd ⊢ ( 𝑘 = 𝑥 → 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) = 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) )
71 67 eleq1d ⊢ ( 𝑘 = 𝑥 → ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 ↔ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 ) )
72 69 eqeq2d ⊢ ( 𝑘 = 𝑥 → ( 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ↔ 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) )
73 71 72 imbi12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) ↔ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) ) )
74 70 73 rabeqbidv ⊢ ( 𝑘 = 𝑥 → { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } = { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } )
75 74 fveq2d ⊢ ( 𝑘 = 𝑥 → ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) = ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) )
76 75 60 fveq12d ⊢ ( 𝑘 = 𝑥 → ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑘 ) ) = ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑥 ) ) )
77 76 cbvixpv ⊢ X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑘 ) ) = X 𝑥 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑥 ) )
78 65 77 eqtrdi ⊢ ( 𝑠 = 𝑔 → X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) = X 𝑥 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑥 ) ) )
79 63 78 eqeq12d ⊢ ( 𝑠 = 𝑔 → ( ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑥 ) ) ) )
80 simpl ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
81 snex ⊢ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ∈ V
82 41 81 unex ⊢ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∈ V
83 ssun2 ⊢ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ⊆ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } )
84 41 uniex ⊢ ∪ ( 𝑔 ‘ 𝑥 ) ∈ V
85 84 pwex ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ V
86 85 snid ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) }
87 83 86 sselii ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } )
88 epttop ⊢ ( ( ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∈ V ∧ 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) → { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ∈ ( TopOn ‘ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) )
89 82 87 88 mp2an ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ∈ ( TopOn ‘ ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) )
90 89 topontopi ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ∈ Top
91 90 a1i ⊢ ( ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) ∧ 𝑥 ∈ dom 𝑔 ) → { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ∈ Top )
92 91 fmpttd ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) : dom 𝑔 ⟶ Top )
93 39 mptex ⊢ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∈ V
94 id ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) )
95 dmeq ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → dom 𝑓 = dom ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) )
96 82 pwex ⊢ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∈ V
97 96 rabex ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ∈ V
98 eqid ⊢ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } )
99 97 98 dmmpti ⊢ dom ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) = dom 𝑔
100 95 99 eqtrdi ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → dom 𝑓 = dom 𝑔 )
101 94 100 feq12d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( 𝑓 : dom 𝑓 ⟶ Top ↔ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) : dom 𝑔 ⟶ Top ) )
102 100 ixpeq1d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = X 𝑘 ∈ dom 𝑔 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) )
103 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( 𝑓 ‘ 𝑘 ) = ( ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ 𝑘 ) )
104 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑘 ) )
105 104 unieqd ⊢ ( 𝑥 = 𝑘 → ∪ ( 𝑔 ‘ 𝑥 ) = ∪ ( 𝑔 ‘ 𝑘 ) )
106 105 pweqd ⊢ ( 𝑥 = 𝑘 → 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) = 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) )
107 106 sneqd ⊢ ( 𝑥 = 𝑘 → { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } = { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
108 104 107 uneq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
109 108 pweqd ⊢ ( 𝑥 = 𝑘 → 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) = 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
110 106 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 ↔ 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 ) )
111 108 eqeq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ↔ 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) )
112 110 111 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) ↔ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) ) )
113 109 112 rabeqbidv ⊢ ( 𝑥 = 𝑘 → { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } = { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } )
114 fvex ⊢ ( 𝑔 ‘ 𝑘 ) ∈ V
115 snex ⊢ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ∈ V
116 114 115 unex ⊢ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∈ V
117 116 pwex ⊢ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∈ V
118 117 rabex ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ∈ V
119 113 98 118 fvmpt ⊢ ( 𝑘 ∈ dom 𝑔 → ( ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ 𝑘 ) = { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } )
120 103 119 sylan9eq ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → ( 𝑓 ‘ 𝑘 ) = { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } )
121 120 unieqd ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → ∪ ( 𝑓 ‘ 𝑘 ) = ∪ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } )
122 ssun2 ⊢ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ⊆ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
123 114 uniex ⊢ ∪ ( 𝑔 ‘ 𝑘 ) ∈ V
124 123 pwex ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ V
125 124 snid ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) }
126 122 125 sselii ⊢ 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
127 epttop ⊢ ( ( ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∈ V ∧ 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) → { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ∈ ( TopOn ‘ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) )
128 116 126 127 mp2an ⊢ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ∈ ( TopOn ‘ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
129 128 toponunii ⊢ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) = ∪ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) }
130 121 129 eqtr4di ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → ∪ ( 𝑓 ‘ 𝑘 ) = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
131 130 pweqd ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
132 131 ixpeq2dva ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑔 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
133 102 132 eqtrd ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) = X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
134 2fveq3 ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( cls ‘ ( ∏t ‘ 𝑓 ) ) = ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) )
135 100 ixpeq1d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) = X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) )
136 134 135 fveq12d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) )
137 100 ixpeq1d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
138 120 fveq2d ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) = ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) )
139 138 fveq1d ⊢ ( ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ∧ 𝑘 ∈ dom 𝑔 ) → ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) = ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
140 139 ixpeq2dva ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑔 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
141 137 140 eqtrd ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
142 136 141 eqeq12d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
143 133 142 raleqbidv ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
144 101 143 imbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) → ( ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ↔ ( ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) : dom 𝑔 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
145 93 144 spcv ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) : dom 𝑔 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
146 80 92 145 sylc ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑘 ∈ dom 𝑔 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) } ) ‘ ( 𝑠 ‘ 𝑘 ) ) )
147 simprl ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → Fun 𝑔 )
148 147 funfnd ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → 𝑔 Fn dom 𝑔 )
149 ssun1 ⊢ ( 𝑔 ‘ 𝑘 ) ⊆ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
150 114 elpw ⊢ ( ( 𝑔 ‘ 𝑘 ) ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ↔ ( 𝑔 ‘ 𝑘 ) ⊆ ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
151 149 150 mpbir ⊢ ( 𝑔 ‘ 𝑘 ) ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
152 151 rgenw ⊢ ∀ 𝑘 ∈ dom 𝑔 ( 𝑔 ‘ 𝑘 ) ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } )
153 38 elixp ⊢ ( 𝑔 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ↔ ( 𝑔 Fn dom 𝑔 ∧ ∀ 𝑘 ∈ dom 𝑔 ( 𝑔 ‘ 𝑘 ) ∈ 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) ) )
154 148 152 153 sylanblrc ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → 𝑔 ∈ X 𝑘 ∈ dom 𝑔 𝒫 ( ( 𝑔 ‘ 𝑘 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑘 ) } ) )
155 79 146 154 rspcdva ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → ( ( cls ‘ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ) ) ‘ X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ dom 𝑔 ( ( cls ‘ { 𝑦 ∈ 𝒫 ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ∣ ( 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) ∈ 𝑦 → 𝑦 = ( ( 𝑔 ‘ 𝑥 ) ∪ { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } ) ) } ) ‘ ( 𝑔 ‘ 𝑥 ) ) )
156 40 42 54 55 56 57 155 dfac14lem ⊢ ( ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) ∧ ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
157 156 ex ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
158 157 alrimiv ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ∀ 𝑔 ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
159 dfac9 ⊢ ( CHOICE ↔ ∀ 𝑔 ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
160 158 159 sylibr ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) → CHOICE )
161 37 160 impbii ⊢ ( CHOICE ↔ ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Top → ∀ 𝑠 ∈ X 𝑘 ∈ dom 𝑓 𝒫 ∪ ( 𝑓 ‘ 𝑘 ) ( ( cls ‘ ( ∏t ‘ 𝑓 ) ) ‘ X 𝑘 ∈ dom 𝑓 ( 𝑠 ‘ 𝑘 ) ) = X 𝑘 ∈ dom 𝑓 ( ( cls ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )