Theorem dfac14 23561

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

Assertion

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

Distinct variable group:   𝑓,𝑘,𝑠

Proof of Theorem dfac14

Dummy variables 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥))
2	1	unieqd 4901	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ∪ (𝑓‘𝑘) = ∪ (𝑓‘𝑥))
3	2	pweqd 4597	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ∪ (𝑓‘𝑥))
4	3	cbvixpv 8934	. . . . . . 7 ⊢ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)
5	4	eleq2i 2827	. . . . . 6 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
6		simplr 768	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓:dom 𝑓⟶Top)
7	6	feqmptd 6952	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
8	7	fveq2d 6885	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (∏t‘𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))
9	8	fveq2d 6885	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))))
10	9	fveq1d 6883	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)))
11		eqid 2736	. . . . . . . 8 ⊢ (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
12		vex 3468	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
13	12	dmex 7910	. . . . . . . . 9 ⊢ dom 𝑓 ∈ V
14	13	a1i 11	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → dom 𝑓 ∈ V)
15	6	ffvelcdmda 7079	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ Top)
16		toptopon2 22861	. . . . . . . . 9 ⊢ ((𝑓‘𝑘) ∈ Top ↔ (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
17	15, 16	sylib 218	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
18		simpr 484	. . . . . . . . . . . 12 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
19	18, 5	sylibr 234	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘))
20		vex 3468	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
21	20	elixp 8923	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘)))
22	21	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
23	19, 22	syl 17	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
24	23	r19.21bi 3238	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
25	24	elpwid 4589	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ⊆ ∪ (𝑓‘𝑘))
26		fvex 6894	. . . . . . . . . 10 ⊢ (𝑠‘𝑘) ∈ V
27	13, 26	iunex 7972	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ V
28		simpll 766	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → CHOICE)
29		acacni 10160	. . . . . . . . . 10 ⊢ ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
30	28, 13, 29	sylancl 586	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → AC dom 𝑓 = V)
31	27, 30	eleqtrrid 2842	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ AC dom 𝑓)
32	11, 14, 17, 25, 31	ptclsg 23558	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
33	10, 32	eqtrd 2771	. . . . . 6 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
34	5, 33	sylan2b 594	. . . . 5 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
35	34	ralrimiva 3133	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Top) → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
36	35	ex 412	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
37	36	alrimiv 1927	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
38		vex 3468	. . . . . . . 8 ⊢ 𝑔 ∈ V
39	38	dmex 7910	. . . . . . 7 ⊢ dom 𝑔 ∈ V
40	39	a1i 11	. . . . . 6 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
41		fvex 6894	. . . . . . 7 ⊢ (𝑔‘𝑥) ∈ V
42	41	a1i 11	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
43		simplrr 777	. . . . . . . 8 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
44		df-nel 3038	. . . . . . . 8 ⊢ (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
45	43, 44	sylib 218	. . . . . . 7 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
46		funforn 6802	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔–onto→ran 𝑔)
47		fof 6795	. . . . . . . . . . . 12 ⊢ (𝑔:dom 𝑔–onto→ran 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
48	46, 47	sylbi 217	. . . . . . . . . . 11 ⊢ (Fun 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
49	48	ad2antrl 728	. . . . . . . . . 10 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
50	49	ffvelcdmda 7079	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
51		eleq1 2823	. . . . . . . . 9 ⊢ ((𝑔‘𝑥) = ∅ → ((𝑔‘𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
52	50, 51	syl5ibcom 245	. . . . . . . 8 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔‘𝑥) = ∅ → ∅ ∈ ran 𝑔))
53	52	necon3bd 2947	. . . . . . 7 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔‘𝑥) ≠ ∅))
54	45, 53	mpd 15	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
55		eqid 2736	. . . . . 6 ⊢ 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑥)
56		eqid 2736	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}
57		eqid 2736	. . . . . 6 ⊢ (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
58		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑔 → (𝑠‘𝑘) = (𝑔‘𝑘))
59	58	ixpeq2dv 8932	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑔‘𝑘))
60		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (𝑔‘𝑘) = (𝑔‘𝑥))
61	60	cbvixpv 8934	. . . . . . . . . 10 ⊢ X𝑘 ∈ dom 𝑔(𝑔‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥)
62	59, 61	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥))
63	62	fveq2d 6885	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)))
64	58	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
65	64	ixpeq2dv 8932	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
66	60	unieqd 4901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ∪ (𝑔‘𝑘) = ∪ (𝑔‘𝑥))
67	66	pweqd 4597	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑔‘𝑘) = 𝒫 ∪ (𝑔‘𝑥))
68	67	sneqd 4618	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → {𝒫 ∪ (𝑔‘𝑘)} = {𝒫 ∪ (𝑔‘𝑥)})
69	60, 68	uneq12d 4149	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
70	69	pweqd 4597	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
71	67	eleq1d 2820	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦))
72	69	eqeq2d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
73	71, 72	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) ↔ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))))
74	70, 73	rabeqbidv 3439	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
75	74	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
76	75, 60	fveq12d 6888	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
77	76	cbvixpv 8934	. . . . . . . . 9 ⊢ X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))
78	65, 77	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
79	63, 78	eqeq12d 2752	. . . . . . 7 ⊢ (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))))
80		simpl 482	. . . . . . . 8 ⊢ ((∀𝑓(𝑓: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 5411	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ∈ V
82	41, 81	unex 7743	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
83		ssun2 4159	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ⊆ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
84	41	uniex 7740	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑔‘𝑥) ∈ V
85	84	pwex 5355	. . . . . . . . . . . . . 14 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ V
86	85	snid 4643	. . . . . . . . . . . . 13 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ {𝒫 ∪ (𝑔‘𝑥)}
87	83, 86	sselii 3960	. . . . . . . . . . . 12 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
88		epttop 22952	. . . . . . . . . . . 12 ⊢ ((((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
89	82, 87, 88	mp2an 692	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
90	89	topontopi 22858	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ Top
91	90	a1i 11	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ Top)
92	91	fmpttd 7110	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top)
93	39	mptex 7220	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∈ V
94		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
95		dmeq 5888	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
96	82	pwex 5355	. . . . . . . . . . . . . 14 ⊢ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
97	96	rabex 5314	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ V
98		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
99	97, 98	dmmpti 6687	. . . . . . . . . . . 12 ⊢ dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = dom 𝑔
100	95, 99	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom 𝑔)
101	94, 100	feq12d 6699	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top))
102	100	ixpeq1d 8928	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘))
103		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓‘𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘))
104		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘))
105	104	unieqd 4901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → ∪ (𝑔‘𝑥) = ∪ (𝑔‘𝑘))
106	105	pweqd 4597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑘 → 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑘))
107	106	sneqd 4618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → {𝒫 ∪ (𝑔‘𝑥)} = {𝒫 ∪ (𝑔‘𝑘)})
108	104, 107	uneq12d 4149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
109	108	pweqd 4597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
110	106	eleq1d 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦))
111	108	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ↔ 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
112	110, 111	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ((𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) ↔ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))))
113	109, 112	rabeqbidv 3439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
114		fvex 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑘) ∈ V
115		snex 5411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ∈ V
116	114, 115	unex 7743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
117	116	pwex 5355	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
118	117	rabex 5314	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ V
119	113, 98, 118	fvmpt 6991	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
120	103, 119	sylan9eq 2791	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
121	120	unieqd 4901	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
122		ssun2 4159	. . . . . . . . . . . . . . . . . 18 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
123	114	uniex 7740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑘) ∈ V
124	123	pwex 5355	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ V
125	124	snid 4643	. . . . . . . . . . . . . . . . . 18 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ {𝒫 ∪ (𝑔‘𝑘)}
126	122, 125	sselii 3960	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
127		epttop 22952	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
128	116, 126, 127	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
129	128	toponunii 22859	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}
130	121, 129	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
131	130	pweqd 4597	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
132	131	ixpeq2dva 8931	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
133	102, 132	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
134		2fveq3 6886	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))))
135	100	ixpeq1d 8928	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑠‘𝑘))
136	134, 135	fveq12d 6888	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)))
137	100	ixpeq1d 8928	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
138	120	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓‘𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}))
139	138	fveq1d 6883	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
140	139	ixpeq2dva 8931	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
141	137, 140	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
142	136, 141	eqeq12d 2752	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
143	133, 142	raleqbidv 3329	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ∀𝑠 ∈ X 𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
144	101, 143	imbi12d 344	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ 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 3589	. . . . . . . 8 ⊢ (∀𝑓(𝑓: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 65	. . . . . . 7 ⊢ ((∀𝑓(𝑓: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 770	. . . . . . . . 9 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
148	147	funfnd 6572	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
149		ssun1 4158	. . . . . . . . . 10 ⊢ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
150	114	elpw 4584	. . . . . . . . . 10 ⊢ ((𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
151	149, 150	mpbir 231	. . . . . . . . 9 ⊢ (𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
152	151	rgenw 3056	. . . . . . . 8 ⊢ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
153	38	elixp 8923	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
154	148, 152, 153	sylanblrc 590	. . . . . . 7 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
155	79, 146, 154	rspcdva 3607	. . . . . 6 ⊢ ((∀𝑓(𝑓: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 23560	. . . . 5 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
157	156	ex 412	. . . 4 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
158	157	alrimiv 1927	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
159		dfac9 10156	. . 3 ⊢ (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
160	158, 159	sylibr 234	. 2 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → CHOICE)
161	37, 160	impbii 209	1 ⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ≠ wne 2933   ∉ wnel 3037  ∀wral 3052  {crab 3420  Vcvv 3464   ∪ cun 3929   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ∪ cuni 4888  ∪ ciun 4972   ↦ cmpt 5206  dom cdm 5659  ran crn 5660  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  –onto→wfo 6534  ‘cfv 6536  Xcixp 8916  AC wacn 9957  CHOICEwac 10134  ∏_tcpt 17457  Topctop 22836  TopOnctopon 22853  clsccl 22961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-1o 8485  df-2o 8486  df-er 8724  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-fin 8968  df-fi 9428  df-card 9958  df-acn 9961  df-ac 10135  df-topgen 17462  df-pt 17463  df-top 22837  df-topon 22854  df-bases 22889  df-cld 22962  df-ntr 22963  df-cls 22964

This theorem is referenced by: (None)