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