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 ‘ ( 𝑓 ‘ 𝑘 ) ) ‘ ( 𝑠 ‘ 𝑘 ) ) ) )