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