Theorem dfac14 23775

Description: Theorem ptcls 23773 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 4885	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ∪ (𝑓‘𝑘) = ∪ (𝑓‘𝑥))
3	2	pweqd 4579	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ∪ (𝑓‘𝑥))
4	3	cbvixpv 8909	. . . . . . 7 ⊢ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)
5	4	eleq2i 2855	. . . . . 6 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
6		simplr 780	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓:dom 𝑓⟶Top)
7	6	feqmptd 6949	. . . . . . . . . 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 2763	. . . . . . . 8 ⊢ (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
12		vex 3459	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
13	12	dmex 7902	. . . . . . . . 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 23075	. . . . . . . . 9 ⊢ ((𝑓‘𝑘) ∈ Top ↔ (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
17	15, 16	sylib 221	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
18	5	bilanri 511	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘))
19		vex 3459	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
20	19	elixp 8898	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘)))
21	20	simprbi 502	. . . . . . . . . . 11 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
22	18, 21	syl 18	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
23	22	r19.21bi 3257	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
24	23	elpwid 4571	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ⊆ ∪ (𝑓‘𝑘))
25		fvex 6894	. . . . . . . . . 10 ⊢ (𝑠‘𝑘) ∈ V
26	13, 25	iunex 7961	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ V
27		simpll 778	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → CHOICE)
28		acacni 10120	. . . . . . . . . 10 ⊢ ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
29	27, 13, 28	sylancl 597	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → AC dom 𝑓 = V)
30	26, 29	eleqtrrid 2870	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ AC dom 𝑓)
31	11, 14, 17, 24, 30	ptclsg 23772	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
32	10, 31	eqtrd 2798	. . . . . 6 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
33	5, 32	sylan2b 605	. . . . 5 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
34	33	ralrimiva 3157	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Top) → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
35	34	ex 417	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
36	35	alrimiv 1957	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
37		vex 3459	. . . . . . . 8 ⊢ 𝑔 ∈ V
38	37	dmex 7902	. . . . . . 7 ⊢ dom 𝑔 ∈ V
39	38	a1i 11	. . . . . 6 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
40		fvex 6894	. . . . . . 7 ⊢ (𝑔‘𝑥) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
42		simplrr 789	. . . . . . . 8 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
43		df-nel 3065	. . . . . . . 8 ⊢ (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
44	42, 43	sylib 221	. . . . . . 7 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
45		funforn 6799	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔–onto→ran 𝑔)
46		fof 6792	. . . . . . . . . . . 12 ⊢ (𝑔:dom 𝑔–onto→ran 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
47	45, 46	sylbi 220	. . . . . . . . . . 11 ⊢ (Fun 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
48	47	ad2antrl 740	. . . . . . . . . 10 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
49	48	ffvelcdmda 7079	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
50		eleq1 2851	. . . . . . . . 9 ⊢ ((𝑔‘𝑥) = ∅ → ((𝑔‘𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
51	49, 50	syl5ibcom 248	. . . . . . . 8 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔‘𝑥) = ∅ → ∅ ∈ ran 𝑔))
52	51	necon3bd 2972	. . . . . . 7 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔‘𝑥) ≠ ∅))
53	44, 52	mpd 16	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
54		eqid 2763	. . . . . 6 ⊢ 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑥)
55		eqid 2763	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}
56		eqid 2763	. . . . . 6 ⊢ (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
57		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑔 → (𝑠‘𝑘) = (𝑔‘𝑘))
58	57	ixpeq2dv 8907	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑔‘𝑘))
59		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (𝑔‘𝑘) = (𝑔‘𝑥))
60	59	cbvixpv 8909	. . . . . . . . . 10 ⊢ X𝑘 ∈ dom 𝑔(𝑔‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥)
61	58, 60	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥))
62	61	fveq2d 6885	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)))
63	57	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
64	63	ixpeq2dv 8907	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
65	59	unieqd 4885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ∪ (𝑔‘𝑘) = ∪ (𝑔‘𝑥))
66	65	pweqd 4579	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑔‘𝑘) = 𝒫 ∪ (𝑔‘𝑥))
67	66	sneqd 4601	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → {𝒫 ∪ (𝑔‘𝑘)} = {𝒫 ∪ (𝑔‘𝑥)})
68	59, 67	uneq12d 4123	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
69	68	pweqd 4579	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
70	66	eleq1d 2848	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦))
71	68	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
72	70, 71	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) ↔ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))))
73	69, 72	rabeqbidv 3434	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
74	73	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
75	74, 59	fveq12d 6888	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
76	75	cbvixpv 8909	. . . . . . . . 9 ⊢ X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))
77	64, 76	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
78	62, 77	eqeq12d 2779	. . . . . . 7 ⊢ (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))))
79		simpl 487	. . . . . . . 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‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
80		snex 5410	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ∈ V
81	40, 80	unex 7742	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
82		ssun2 4132	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ⊆ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
83	40	uniex 7739	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑔‘𝑥) ∈ V
84	83	pwex 5351	. . . . . . . . . . . . . 14 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ V
85	84	snid 4628	. . . . . . . . . . . . 13 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ {𝒫 ∪ (𝑔‘𝑥)}
86	82, 85	sselii 3934	. . . . . . . . . . . 12 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
87		epttop 23166	. . . . . . . . . . . 12 ⊢ ((((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
88	81, 86, 87	mp2an 704	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
89	88	topontopi 23072	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ Top
90	89	a1i 11	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ Top)
91	90	fmpttd 7110	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top)
92	38	mptex 7221	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∈ V
93		id 23	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
94		dmeq 5893	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
95	81	pwex 5351	. . . . . . . . . . . . . 14 ⊢ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
96	95	rabex 5309	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ V
97		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
98	96, 97	dmmpti 6679	. . . . . . . . . . . 12 ⊢ dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = dom 𝑔
99	94, 98	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom 𝑔)
100	93, 99	feq12d 6693	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top))
101	99	ixpeq1d 8903	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘))
102		fveq1 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓‘𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘))
103		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘))
104	103	unieqd 4885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → ∪ (𝑔‘𝑥) = ∪ (𝑔‘𝑘))
105	104	pweqd 4579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑘 → 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑘))
106	105	sneqd 4601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → {𝒫 ∪ (𝑔‘𝑥)} = {𝒫 ∪ (𝑔‘𝑘)})
107	103, 106	uneq12d 4123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
108	107	pweqd 4579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
109	105	eleq1d 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦))
110	107	eqeq2d 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ↔ 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ((𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) ↔ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))))
112	108, 111	rabeqbidv 3434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
113		fvex 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑘) ∈ V
114		snex 5410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ∈ V
115	113, 114	unex 7742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
116	115	pwex 5351	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
117	116	rabex 5309	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ V
118	112, 97, 117	fvmpt 6989	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
119	102, 118	sylan9eq 2818	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
120	119	unieqd 4885	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
121		ssun2 4132	. . . . . . . . . . . . . . . . . 18 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
122	113	uniex 7739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑘) ∈ V
123	122	pwex 5351	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ V
124	123	snid 4628	. . . . . . . . . . . . . . . . . 18 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ {𝒫 ∪ (𝑔‘𝑘)}
125	121, 124	sselii 3934	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
126		epttop 23166	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
127	115, 125, 126	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
128	127	toponunii 23073	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}
129	120, 128	eqtr4di 2816	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
130	129	pweqd 4579	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
131	130	ixpeq2dva 8906	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
132	101, 131	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
133		2fveq3 6886	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))))
134	99	ixpeq1d 8903	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑠‘𝑘))
135	133, 134	fveq12d 6888	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)))
136	99	ixpeq1d 8903	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
137	119	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓‘𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}))
138	137	fveq1d 6883	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
139	138	ixpeq2dva 8906	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
140	136, 139	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
141	135, 140	eqeq12d 2779	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
142	132, 141	raleqbidv 3338	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ∀𝑠 ∈ X 𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
143	100, 142	imbi12d 347	. . . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))))
144	92, 143	spcv 3564	. . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
145	79, 91, 144	sylc 66	. . . . . . 7 ⊢ ((∀𝑓(𝑓: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 782	. . . . . . . . 9 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
147	146	funfnd 6567	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
148		ssun1 4131	. . . . . . . . . 10 ⊢ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
149	113	elpw 4566	. . . . . . . . . 10 ⊢ ((𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
150	148, 149	mpbir 234	. . . . . . . . 9 ⊢ (𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
151	150	rgenw 3083	. . . . . . . 8 ⊢ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
152	37	elixp 8898	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
153	147, 151, 152	sylanblrc 601	. . . . . . 7 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
154	78, 145, 153	rspcdva 3582	. . . . . 6 ⊢ ((∀𝑓(𝑓: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 23774	. . . . 5 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
156	155	ex 417	. . . 4 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
157	156	alrimiv 1957	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
158		dfac9 10116	. . 3 ⊢ (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
159	157, 158	sylibr 237	. 2 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → CHOICE)
160	36, 159	impbii 212	1 ⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ≠ wne 2958   ∉ wnel 3064  ∀wral 3079  {crab 3416  Vcvv 3455   ∪ cun 3903   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4562  {csn 4589  ∪ cuni 4872  ∪ ciun 4956   ↦ cmpt 5192  dom cdm 5661  ran crn 5662  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  –onto→wfo 6534  ‘cfv 6536  Xcixp 8891  AC wacn 9920  CHOICEwac 10095  ∏_tcpt 17486  Topctop 23050  TopOnctopon 23067  clsccl 23175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  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 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9367  df-card 9921  df-acn 9924  df-ac 10096  df-topgen 17491  df-pt 17492  df-top 23051  df-topon 23068  df-bases 23103  df-cld 23176  df-ntr 23177  df-cls 23178

This theorem is referenced by: (None)