Theorem dfac14 23845

Description: Theorem ptcls 23843 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 6879	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥))
2	1	unieqd 4880	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ∪ (𝑓‘𝑘) = ∪ (𝑓‘𝑥))
3	2	pweqd 4574	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ∪ (𝑓‘𝑥))
4	3	cbvixpv 8923	. . . . . . 7 ⊢ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)
5	4	eleq2i 2852	. . . . . 6 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
6		simplr 781	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓:dom 𝑓⟶Top)
7	6	feqmptd 6947	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
8	7	fveq2d 6883	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (∏t‘𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))
9	8	fveq2d 6883	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))))
10	9	fveq1d 6881	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)))
11		eqid 2760	. . . . . . . 8 ⊢ (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
12		vex 3454	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
13	12	dmex 7907	. . . . . . . . 9 ⊢ dom 𝑓 ∈ V
14	13	a1i 11	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → dom 𝑓 ∈ V)
15	6	ffvelcdmda 7078	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ Top)
16		toptopon2 23144	. . . . . . . . 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 3454	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
20	19	elixp 8912	. . . . . . . . . . . 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 3254	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
24	23	elpwid 4566	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ⊆ ∪ (𝑓‘𝑘))
25		fvex 6892	. . . . . . . . . 10 ⊢ (𝑠‘𝑘) ∈ V
26	13, 25	iunex 7966	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ V
27		simpll 779	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → CHOICE)
28		acacni 10144	. . . . . . . . . 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 2867	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ AC dom 𝑓)
31	11, 14, 17, 24, 30	ptclsg 23842	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
32	10, 31	eqtrd 2795	. . . . . 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 3154	. . . 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 3454	. . . . . . . 8 ⊢ 𝑔 ∈ V
38	37	dmex 7907	. . . . . . 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 6892	. . . . . . 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 3062	. . . . . . . 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 6797	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔–onto→ran 𝑔)
46		fof 6790	. . . . . . . . . . . 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 7078	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
50		eleq1 2848	. . . . . . . . 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 2969	. . . . . . 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 2760	. . . . . 6 ⊢ 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑥)
55		eqid 2760	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}
56		eqid 2760	. . . . . 6 ⊢ (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
57		fveq1 6878	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑔 → (𝑠‘𝑘) = (𝑔‘𝑘))
58	57	ixpeq2dv 8921	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑔‘𝑘))
59		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (𝑔‘𝑘) = (𝑔‘𝑥))
60	59	cbvixpv 8923	. . . . . . . . . 10 ⊢ X𝑘 ∈ dom 𝑔(𝑔‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥)
61	58, 60	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥))
62	61	fveq2d 6883	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)))
63	57	fveq2d 6883	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
64	63	ixpeq2dv 8921	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
65	59	unieqd 4880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ∪ (𝑔‘𝑘) = ∪ (𝑔‘𝑥))
66	65	pweqd 4574	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑔‘𝑘) = 𝒫 ∪ (𝑔‘𝑥))
67	66	sneqd 4596	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → {𝒫 ∪ (𝑔‘𝑘)} = {𝒫 ∪ (𝑔‘𝑥)})
68	59, 67	uneq12d 4116	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
69	68	pweqd 4574	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
70	66	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦))
71	68	eqeq2d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
72	70, 71	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) ↔ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))))
73	69, 72	rabeqbidv 3429	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
74	73	fveq2d 6883	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
75	74, 59	fveq12d 6886	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
76	75	cbvixpv 8923	. . . . . . . . 9 ⊢ X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))
77	64, 76	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
78	62, 77	eqeq12d 2776	. . . . . . 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 5404	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ∈ V
81	40, 80	unex 7747	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
82		ssun2 4125	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ⊆ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
83	40	uniex 7744	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑔‘𝑥) ∈ V
84	83	pwex 5345	. . . . . . . . . . . . . 14 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ V
85	84	snid 4623	. . . . . . . . . . . . 13 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ {𝒫 ∪ (𝑔‘𝑥)}
86	82, 85	sselii 3928	. . . . . . . . . . . 12 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
87		epttop 23235	. . . . . . . . . . . 12 ⊢ ((((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
88	81, 86, 87	mp2an 705	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
89	88	topontopi 23141	. . . . . . . . . 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 7109	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top)
92	38	mptex 7223	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∈ V
93		id 23	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
94		dmeq 5887	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
95	81	pwex 5345	. . . . . . . . . . . . . 14 ⊢ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
96	95	rabex 5303	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ V
97		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
98	96, 97	dmmpti 6677	. . . . . . . . . . . 12 ⊢ dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = dom 𝑔
99	94, 98	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom 𝑔)
100	93, 99	feq12d 6691	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top))
101	99	ixpeq1d 8917	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘))
102		fveq1 6878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓‘𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘))
103		fveq2 6879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘))
104	103	unieqd 4880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → ∪ (𝑔‘𝑥) = ∪ (𝑔‘𝑘))
105	104	pweqd 4574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑘 → 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑘))
106	105	sneqd 4596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → {𝒫 ∪ (𝑔‘𝑥)} = {𝒫 ∪ (𝑔‘𝑘)})
107	103, 106	uneq12d 4116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
108	107	pweqd 4574	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
109	105	eleq1d 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦))
110	107	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ↔ 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ((𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) ↔ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))))
112	108, 111	rabeqbidv 3429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
113		fvex 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑘) ∈ V
114		snex 5404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ∈ V
115	113, 114	unex 7747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
116	115	pwex 5345	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
117	116	rabex 5303	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ V
118	112, 97, 117	fvmpt 6987	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
119	102, 118	sylan9eq 2815	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
120	119	unieqd 4880	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
121		ssun2 4125	. . . . . . . . . . . . . . . . . 18 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
122	113	uniex 7744	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑘) ∈ V
123	122	pwex 5345	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ V
124	123	snid 4623	. . . . . . . . . . . . . . . . . 18 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ {𝒫 ∪ (𝑔‘𝑘)}
125	121, 124	sselii 3928	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
126		epttop 23235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
127	115, 125, 126	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
128	127	toponunii 23142	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}
129	120, 128	eqtr4di 2813	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
130	129	pweqd 4574	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
131	130	ixpeq2dva 8920	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
132	101, 131	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
133		2fveq3 6884	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))))
134	99	ixpeq1d 8917	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑠‘𝑘))
135	133, 134	fveq12d 6886	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)))
136	99	ixpeq1d 8917	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
137	119	fveq2d 6883	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓‘𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}))
138	137	fveq1d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
139	138	ixpeq2dva 8920	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
140	136, 139	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
141	135, 140	eqeq12d 2776	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
142	132, 141	raleqbidv 3334	. . . . . . . . . 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 3559	. . . . . . . 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 6565	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
148		ssun1 4124	. . . . . . . . . 10 ⊢ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
149	113	elpw 4561	. . . . . . . . . 10 ⊢ ((𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
150	148, 149	mpbir 234	. . . . . . . . 9 ⊢ (𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
151	150	rgenw 3080	. . . . . . . 8 ⊢ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
152	37	elixp 8912	. . . . . . . 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 3577	. . . . . 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 23844	. . . . 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 10140	. . 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 2145   ≠ wne 2955   ∉ wnel 3061  ∀wral 3076  {crab 3412  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867  ∪ ciun 4951   ↦ cmpt 5186  dom cdm 5655  ran crn 5656  Fun wfun 6527   Fn wfn 6528  ⟶wf 6529  –onto→wfo 6531  ‘cfv 6533  Xcixp 8905  AC wacn 9944  CHOICEwac 10119  ∏_tcpt 17524  Topctop 23119  TopOnctopon 23136  clsccl 23244

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-1o 8456  df-2o 8457  df-er 8697  df-map 8829  df-ixp 8906  df-en 8954  df-dom 8955  df-fin 8957  df-fi 9382  df-card 9945  df-acn 9948  df-ac 10120  df-topgen 17529  df-pt 17530  df-top 23120  df-topon 23137  df-bases 23172  df-cld 23245  df-ntr 23246  df-cls 23247

This theorem is used by: (None)