Theorem dfac14 23828

Description: Theorem ptcls 23826 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 6885	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥))
2	1	unieqd 4887	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ∪ (𝑓‘𝑘) = ∪ (𝑓‘𝑥))
3	2	pweqd 4581	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ∪ (𝑓‘𝑥))
4	3	cbvixpv 8919	. . . . . . 7 ⊢ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)
5	4	eleq2i 2857	. . . . . 6 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
6		simplr 781	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓:dom 𝑓⟶Top)
7	6	feqmptd 6953	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
8	7	fveq2d 6889	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (∏t‘𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))
9	8	fveq2d 6889	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))))
10	9	fveq1d 6887	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)))
11		eqid 2765	. . . . . . . 8 ⊢ (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
12		vex 3461	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
13	12	dmex 7912	. . . . . . . . 9 ⊢ dom 𝑓 ∈ V
14	13	a1i 11	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → dom 𝑓 ∈ V)
15	6	ffvelcdmda 7083	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ Top)
16		toptopon2 23127	. . . . . . . . 9 ⊢ ((𝑓‘𝑘) ∈ Top ↔ (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
17	15, 16	sylib 221	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ (TopOn‘∪ (𝑓‘𝑘)))
18	5	bilanri 512	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘))
19		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
20	19	elixp 8908	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘)))
21	20	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
22	18, 21	syl 18	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
23	22	r19.21bi 3259	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
24	23	elpwid 4573	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ⊆ ∪ (𝑓‘𝑘))
25		fvex 6898	. . . . . . . . . 10 ⊢ (𝑠‘𝑘) ∈ V
26	13, 25	iunex 7971	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ V
27		simpll 779	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → CHOICE)
28		acacni 10140	. . . . . . . . . 10 ⊢ ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
29	27, 13, 28	sylancl 598	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → AC dom 𝑓 = V)
30	26, 29	eleqtrrid 2872	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ AC dom 𝑓)
31	11, 14, 17, 24, 30	ptclsg 23825	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
32	10, 31	eqtrd 2800	. . . . . 6 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
33	5, 32	sylan2b 606	. . . . 5 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
34	33	ralrimiva 3159	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Top) → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
35	34	ex 418	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
36	35	alrimiv 1960	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
37		vex 3461	. . . . . . . 8 ⊢ 𝑔 ∈ V
38	37	dmex 7912	. . . . . . 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 6898	. . . . . . 7 ⊢ (𝑔‘𝑥) ∈ V
41	40	a1i 11	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
42		simplrr 790	. . . . . . . 8 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
43		df-nel 3067	. . . . . . . 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 6803	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔–onto→ran 𝑔)
46		fof 6796	. . . . . . . . . . . 12 ⊢ (𝑔:dom 𝑔–onto→ran 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
47	45, 46	sylbi 220	. . . . . . . . . . 11 ⊢ (Fun 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
48	47	ad2antrl 741	. . . . . . . . . 10 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
49	48	ffvelcdmda 7083	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
50		eleq1 2853	. . . . . . . . 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 2974	. . . . . . 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 2765	. . . . . 6 ⊢ 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑥)
55		eqid 2765	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}
56		eqid 2765	. . . . . 6 ⊢ (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
57		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑔 → (𝑠‘𝑘) = (𝑔‘𝑘))
58	57	ixpeq2dv 8917	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑔‘𝑘))
59		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (𝑔‘𝑘) = (𝑔‘𝑥))
60	59	cbvixpv 8919	. . . . . . . . . 10 ⊢ X𝑘 ∈ dom 𝑔(𝑔‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥)
61	58, 60	eqtrdi 2816	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥))
62	61	fveq2d 6889	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)))
63	57	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
64	63	ixpeq2dv 8917	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
65	59	unieqd 4887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ∪ (𝑔‘𝑘) = ∪ (𝑔‘𝑥))
66	65	pweqd 4581	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑔‘𝑘) = 𝒫 ∪ (𝑔‘𝑥))
67	66	sneqd 4603	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → {𝒫 ∪ (𝑔‘𝑘)} = {𝒫 ∪ (𝑔‘𝑥)})
68	59, 67	uneq12d 4123	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
69	68	pweqd 4581	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
70	66	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦))
71	68	eqeq2d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
72	70, 71	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) ↔ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))))
73	69, 72	rabeqbidv 3436	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
74	73	fveq2d 6889	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
75	74, 59	fveq12d 6892	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
76	75	cbvixpv 8919	. . . . . . . . 9 ⊢ X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))
77	64, 76	eqtrdi 2816	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
78	62, 77	eqeq12d 2781	. . . . . . 7 ⊢ (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))))
79		simpl 488	. . . . . . . 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 5412	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ∈ V
81	40, 80	unex 7752	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
82		ssun2 4132	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ⊆ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
83	40	uniex 7749	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑔‘𝑥) ∈ V
84	83	pwex 5353	. . . . . . . . . . . . . 14 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ V
85	84	snid 4630	. . . . . . . . . . . . 13 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ {𝒫 ∪ (𝑔‘𝑥)}
86	82, 85	sselii 3935	. . . . . . . . . . . 12 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
87		epttop 23218	. . . . . . . . . . . 12 ⊢ ((((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
88	81, 86, 87	mp2an 705	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
89	88	topontopi 23124	. . . . . . . . . 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 7114	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top)
92	38	mptex 7228	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∈ V
93		id 23	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
94		dmeq 5895	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
95	81	pwex 5353	. . . . . . . . . . . . . 14 ⊢ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
96	95	rabex 5311	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ V
97		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
98	96, 97	dmmpti 6683	. . . . . . . . . . . 12 ⊢ dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = dom 𝑔
99	94, 98	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom 𝑔)
100	93, 99	feq12d 6697	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top))
101	99	ixpeq1d 8913	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘))
102		fveq1 6884	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓‘𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘))
103		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘))
104	103	unieqd 4887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → ∪ (𝑔‘𝑥) = ∪ (𝑔‘𝑘))
105	104	pweqd 4581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑘 → 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑘))
106	105	sneqd 4603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → {𝒫 ∪ (𝑔‘𝑥)} = {𝒫 ∪ (𝑔‘𝑘)})
107	103, 106	uneq12d 4123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
108	107	pweqd 4581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
109	105	eleq1d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦))
110	107	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ↔ 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ((𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) ↔ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))))
112	108, 111	rabeqbidv 3436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
113		fvex 6898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑘) ∈ V
114		snex 5412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ∈ V
115	113, 114	unex 7752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
116	115	pwex 5353	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
117	116	rabex 5311	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ V
118	112, 97, 117	fvmpt 6993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
119	102, 118	sylan9eq 2820	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
120	119	unieqd 4887	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
121		ssun2 4132	. . . . . . . . . . . . . . . . . 18 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
122	113	uniex 7749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑘) ∈ V
123	122	pwex 5353	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ V
124	123	snid 4630	. . . . . . . . . . . . . . . . . 18 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ {𝒫 ∪ (𝑔‘𝑘)}
125	121, 124	sselii 3935	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
126		epttop 23218	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
127	115, 125, 126	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
128	127	toponunii 23125	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}
129	120, 128	eqtr4di 2818	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
130	129	pweqd 4581	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
131	130	ixpeq2dva 8916	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
132	101, 131	eqtrd 2800	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
133		2fveq3 6890	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))))
134	99	ixpeq1d 8913	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑠‘𝑘))
135	133, 134	fveq12d 6892	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)))
136	99	ixpeq1d 8913	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
137	119	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓‘𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}))
138	137	fveq1d 6887	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
139	138	ixpeq2dva 8916	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
140	136, 139	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
141	135, 140	eqeq12d 2781	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
142	132, 141	raleqbidv 3340	. . . . . . . . . 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 3566	. . . . . . . 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 783	. . . . . . . . 9 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
147	146	funfnd 6571	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
148		ssun1 4131	. . . . . . . . . 10 ⊢ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
149	113	elpw 4568	. . . . . . . . . 10 ⊢ ((𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
150	148, 149	mpbir 234	. . . . . . . . 9 ⊢ (𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
151	150	rgenw 3085	. . . . . . . 8 ⊢ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
152	37	elixp 8908	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
153	147, 151, 152	sylanblrc 602	. . . . . . 7 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
154	78, 145, 153	rspcdva 3584	. . . . . 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 23827	. . . . 5 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
156	155	ex 418	. . . 4 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
157	156	alrimiv 1960	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
158		dfac9 10136	. . 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‘(𝑓‘𝑘))‘(𝑠‘𝑘))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2146   ≠ wne 2960   ∉ wnel 3066  ∀wral 3081  {crab 3418  Vcvv 3457   ∪ cun 3904   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  {csn 4591  ∪ cuni 4874  ∪ ciun 4958   ↦ cmpt 5194  dom cdm 5663  ran crn 5664  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  –onto→wfo 6538  ‘cfv 6540  Xcixp 8901  AC wacn 9940  CHOICEwac 10115  ∏_tcpt 17515  Topctop 23102  TopOnctopon 23119  clsccl 23227

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-ixp 8902  df-en 8950  df-dom 8951  df-fin 8953  df-fi 9378  df-card 9941  df-acn 9944  df-ac 10116  df-topgen 17520  df-pt 17521  df-top 23103  df-topon 23120  df-bases 23155  df-cld 23228  df-ntr 23229  df-cls 23230

This theorem is used by: (None)