Theorem dfac14 23596

Description: Theorem ptcls 23594 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 6835	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝑓‘𝑘) = (𝑓‘𝑥))
2	1	unieqd 4864	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ∪ (𝑓‘𝑘) = ∪ (𝑓‘𝑥))
3	2	pweqd 4559	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ∪ (𝑓‘𝑥))
4	3	cbvixpv 8857	. . . . . . 7 ⊢ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)
5	4	eleq2i 2829	. . . . . 6 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥))
6		simplr 769	. . . . . . . . . . 11 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓:dom 𝑓⟶Top)
7	6	feqmptd 6903	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
8	7	fveq2d 6839	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (∏t‘𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))
9	8	fveq2d 6839	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))))
10	9	fveq1d 6837	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)))
11		eqid 2737	. . . . . . . 8 ⊢ (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘)))
12		vex 3434	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
13	12	dmex 7854	. . . . . . . . 9 ⊢ dom 𝑓 ∈ V
14	13	a1i 11	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → dom 𝑓 ∈ V)
15	6	ffvelcdmda 7031	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓‘𝑘) ∈ Top)
16		toptopon2 22896	. . . . . . . . 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 3434	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
21	20	elixp 8846	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘)))
22	21	simprbi 497	. . . . . . . . . . 11 ⊢ (𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
23	19, 22	syl 17	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
24	23	r19.21bi 3230	. . . . . . . . 9 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ∈ 𝒫 ∪ (𝑓‘𝑘))
25	24	elpwid 4551	. . . . . . . 8 ⊢ ((((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠‘𝑘) ⊆ ∪ (𝑓‘𝑘))
26		fvex 6848	. . . . . . . . . 10 ⊢ (𝑠‘𝑘) ∈ V
27	13, 26	iunex 7915	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ V
28		simpll 767	. . . . . . . . . 10 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → CHOICE)
29		acacni 10057	. . . . . . . . . 10 ⊢ ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
30	28, 13, 29	sylancl 587	. . . . . . . . 9 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → AC dom 𝑓 = V)
31	27, 30	eleqtrrid 2844	. . . . . . . 8 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ∪ 𝑘 ∈ dom 𝑓(𝑠‘𝑘) ∈ AC dom 𝑓)
32	11, 14, 17, 25, 31	ptclsg 23593	. . . . . . 7 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓‘𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
33	10, 32	eqtrd 2772	. . . . . 6 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑥 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑥)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
34	5, 33	sylan2b 595	. . . . 5 ⊢ (((CHOICE ∧ 𝑓:dom 𝑓⟶Top) ∧ 𝑠 ∈ X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
35	34	ralrimiva 3130	. . . 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 1929	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
38		vex 3434	. . . . . . . 8 ⊢ 𝑔 ∈ V
39	38	dmex 7854	. . . . . . 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 6848	. . . . . . 7 ⊢ (𝑔‘𝑥) ∈ V
42	41	a1i 11	. . . . . 6 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
43		simplrr 778	. . . . . . . 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 6754	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 ↔ 𝑔:dom 𝑔–onto→ran 𝑔)
47		fof 6747	. . . . . . . . . . . 12 ⊢ (𝑔:dom 𝑔–onto→ran 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
48	46, 47	sylbi 217	. . . . . . . . . . 11 ⊢ (Fun 𝑔 → 𝑔:dom 𝑔⟶ran 𝑔)
49	48	ad2antrl 729	. . . . . . . . . 10 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
50	49	ffvelcdmda 7031	. . . . . . . . 9 ⊢ (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
51		eleq1 2825	. . . . . . . . 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 2737	. . . . . 6 ⊢ 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑥)
56		eqid 2737	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}
57		eqid 2737	. . . . . 6 ⊢ (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
58		fveq1 6834	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑔 → (𝑠‘𝑘) = (𝑔‘𝑘))
59	58	ixpeq2dv 8855	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑔‘𝑘))
60		fveq2 6835	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (𝑔‘𝑘) = (𝑔‘𝑥))
61	60	cbvixpv 8857	. . . . . . . . . 10 ⊢ X𝑘 ∈ dom 𝑔(𝑔‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥)
62	59, 61	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔(𝑠‘𝑘) = X𝑥 ∈ dom 𝑔(𝑔‘𝑥))
63	62	fveq2d 6839	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔‘𝑥)))
64	58	fveq2d 6839	. . . . . . . . . 10 ⊢ (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
65	64	ixpeq2dv 8855	. . . . . . . . 9 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)))
66	60	unieqd 4864	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ∪ (𝑔‘𝑘) = ∪ (𝑔‘𝑥))
67	66	pweqd 4559	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → 𝒫 ∪ (𝑔‘𝑘) = 𝒫 ∪ (𝑔‘𝑥))
68	67	sneqd 4580	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → {𝒫 ∪ (𝑔‘𝑘)} = {𝒫 ∪ (𝑔‘𝑥)})
69	60, 68	uneq12d 4110	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
70	69	pweqd 4559	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
71	67	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦))
72	69	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
73	71, 72	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) ↔ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))))
74	70, 73	rabeqbidv 3408	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
75	74	fveq2d 6839	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
76	75, 60	fveq12d 6842	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
77	76	cbvixpv 8857	. . . . . . . . 9 ⊢ X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑔‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥))
78	65, 77	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑠 = 𝑔 → X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘(𝑔‘𝑥)))
79	63, 78	eqeq12d 2753	. . . . . . 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 5377	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ∈ V
82	41, 81	unex 7692	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
83		ssun2 4120	. . . . . . . . . . . . 13 ⊢ {𝒫 ∪ (𝑔‘𝑥)} ⊆ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
84	41	uniex 7689	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑔‘𝑥) ∈ V
85	84	pwex 5318	. . . . . . . . . . . . . 14 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ V
86	85	snid 4607	. . . . . . . . . . . . 13 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ {𝒫 ∪ (𝑔‘𝑥)}
87	83, 86	sselii 3919	. . . . . . . . . . . 12 ⊢ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})
88		epttop 22987	. . . . . . . . . . . 12 ⊢ ((((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑥) ∈ ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})))
89	82, 87, 88	mp2an 693	. . . . . . . . . . 11 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ (TopOn‘((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))
90	89	topontopi 22893	. . . . . . . . . 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 7062	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top)
93	39	mptex 7172	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∈ V
94		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
95		dmeq 5853	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))
96	82	pwex 5318	. . . . . . . . . . . . . 14 ⊢ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∈ V
97	96	rabex 5277	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} ∈ V
98		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})
99	97, 98	dmmpti 6637	. . . . . . . . . . . 12 ⊢ dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) = dom 𝑔
100	95, 99	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → dom 𝑓 = dom 𝑔)
101	94, 100	feq12d 6651	. . . . . . . . . 10 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}):dom 𝑔⟶Top))
102	100	ixpeq1d 8851	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘))
103		fveq1 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (𝑓‘𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘))
104		fveq2 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘))
105	104	unieqd 4864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑘 → ∪ (𝑔‘𝑥) = ∪ (𝑔‘𝑘))
106	105	pweqd 4559	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑘 → 𝒫 ∪ (𝑔‘𝑥) = 𝒫 ∪ (𝑔‘𝑘))
107	106	sneqd 4580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑘 → {𝒫 ∪ (𝑔‘𝑥)} = {𝒫 ∪ (𝑔‘𝑘)})
108	104, 107	uneq12d 4110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
109	108	pweqd 4559	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
110	106	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 ↔ 𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦))
111	108	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑘 → (𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ↔ 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
112	110, 111	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ((𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)})) ↔ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))))
113	109, 112	rabeqbidv 3408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
114		fvex 6848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑘) ∈ V
115		snex 5377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ∈ V
116	114, 115	unex 7692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
117	116	pwex 5318	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V
118	117	rabex 5277	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ V
119	113, 98, 118	fvmpt 6942	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
120	103, 119	sylan9eq 2792	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
121	120	unieqd 4864	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})
122		ssun2 4120	. . . . . . . . . . . . . . . . . 18 ⊢ {𝒫 ∪ (𝑔‘𝑘)} ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
123	114	uniex 7689	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑘) ∈ V
124	123	pwex 5318	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ V
125	124	snid 4607	. . . . . . . . . . . . . . . . . 18 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ {𝒫 ∪ (𝑔‘𝑘)}
126	122, 125	sselii 3919	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
127		epttop 22987	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∈ V ∧ 𝒫 ∪ (𝑔‘𝑘) ∈ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
128	116, 126, 127	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))} ∈ (TopOn‘((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
129	128	toponunii 22894	. . . . . . . . . . . . . . 15 ⊢ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) = ∪ {𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}
130	121, 129	eqtr4di 2790	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ∪ (𝑓‘𝑘) = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
131	130	pweqd 4559	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 ∪ (𝑓‘𝑘) = 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
132	131	ixpeq2dva 8854	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
133	102, 132	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
134		2fveq3 6840	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (cls‘(∏t‘𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}))))
135	100	ixpeq1d 8851	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠‘𝑘) = X𝑘 ∈ dom 𝑔(𝑠‘𝑘))
136	134, 135	fveq12d 6842	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → ((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)))
137	100	ixpeq1d 8851	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))
138	120	fveq2d 6839	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓‘𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))}))
139	138	fveq1d 6837	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
140	139	ixpeq2dva 8854	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
141	137, 140	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘)))
142	136, 141	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))}) → (((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}) ∣ (𝒫 ∪ (𝑔‘𝑥) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑥) ∪ {𝒫 ∪ (𝑔‘𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ∣ (𝒫 ∪ (𝑔‘𝑘) ∈ 𝑦 → 𝑦 = ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))})‘(𝑠‘𝑘))))
143	133, 142	raleqbidv 3312	. . . . . . . . . 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 3548	. . . . . . . 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 771	. . . . . . . . 9 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
148	147	funfnd 6524	. . . . . . . 8 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
149		ssun1 4119	. . . . . . . . . 10 ⊢ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
150	114	elpw 4546	. . . . . . . . . 10 ⊢ ((𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔‘𝑘) ⊆ ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
151	149, 150	mpbir 231	. . . . . . . . 9 ⊢ (𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
152	151	rgenw 3056	. . . . . . . 8 ⊢ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})
153	38	elixp 8846	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔‘𝑘) ∈ 𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)})))
154	148, 152, 153	sylanblrc 591	. . . . . . 7 ⊢ ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 ∈ X𝑘 ∈ dom 𝑔𝒫 ((𝑔‘𝑘) ∪ {𝒫 ∪ (𝑔‘𝑘)}))
155	79, 146, 154	rspcdva 3566	. . . . . 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 23595	. . . . 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 1929	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
159		dfac9 10053	. . 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 1540   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∉ wnel 3037  ∀wral 3052  {crab 3390  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542  {csn 4568  ∪ cuni 4851  ∪ ciun 4934   ↦ cmpt 5167  dom cdm 5625  ran crn 5626  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491  ‘cfv 6493  Xcixp 8839  AC wacn 9856  CHOICEwac 10031  ∏_tcpt 17395  Topctop 22871  TopOnctopon 22888  clsccl 22996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-ixp 8840  df-en 8888  df-dom 8889  df-fin 8891  df-fi 9318  df-card 9857  df-acn 9860  df-ac 10032  df-topgen 17400  df-pt 17401  df-top 22872  df-topon 22889  df-bases 22924  df-cld 22997  df-ntr 22998  df-cls 22999

This theorem is referenced by: (None)