dfac14

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

		Ref	Expression
	Assertion	dfac14	$⊢ CHOICE \leftrightarrow \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ k = x \to f (k) = f (x)$
2	1	unieqd	$⊢ k = x \to ⋃ f (k) = ⋃ f (x)$
3	2	pweqd	$⊢ k = x \to 𝒫 ⋃ f (k) = 𝒫 ⋃ f (x)$
4	3	cbvixpv	$⊢ \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) = \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)$
5	4	eleq2i	$⊢ s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) \leftrightarrow s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)$
6		simplr	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to f : dom f ⟶ Top$
7	6	feqmptd	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to f = (k \in dom f ⟼ f (k))$
8	7	fveq2d	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to \prod_{𝑡} (f) = \prod_{𝑡} ((k \in dom f ⟼ f (k)))$
9	8	fveq2d	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to cls (\prod_{𝑡} (f)) = cls (\prod_{𝑡} ((k \in dom f ⟼ f (k))))$
10	9	fveq1d	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = cls (\prod_{𝑡} ((k \in dom f ⟼ f (k)))) (\underset{k \in dom f}{⨉} s (k))$
11		eqid	$⊢ \prod_{𝑡} ((k \in dom f ⟼ f (k))) = \prod_{𝑡} ((k \in dom f ⟼ f (k)))$
12		vex	$⊢ f \in V$
13	12	dmex	$⊢ dom f \in V$
14	13	a1i	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to dom f \in V$
15	6	ffvelrnda	$⊢ (((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \land k \in dom f) \to f (k) \in Top$
16		toptopon2	$⊢ f (k) \in Top \leftrightarrow f (k) \in TopOn (⋃ f (k))$
17	15 16	sylib	$⊢ (((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \land k \in dom f) \to f (k) \in TopOn (⋃ f (k))$
18		simpr	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)$
19	18 5	sylibr	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k)$
20		vex	$⊢ s \in V$
21	20	elixp	$⊢ s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) \leftrightarrow (s Fn dom f \land \forall k \in dom f s (k) \in 𝒫 ⋃ f (k))$
22	21	simprbi	$⊢ s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) \to \forall k \in dom f s (k) \in 𝒫 ⋃ f (k)$
23	19 22	syl	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to \forall k \in dom f s (k) \in 𝒫 ⋃ f (k)$
24	23	r19.21bi	$⊢ (((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \land k \in dom f) \to s (k) \in 𝒫 ⋃ f (k)$
25	24	elpwid	$⊢ (((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \land k \in dom f) \to s (k) \subseteq ⋃ f (k)$
26		fvex	$⊢ s (k) \in V$
27	13 26	iunex	$⊢ ⋃_{k \in dom f} s (k) \in V$
28		simpll	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to CHOICE$
29		acacni	$⊢ (CHOICE \land dom f \in V) \to \underline{AC} dom f = V$
30	28 13 29	sylancl	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to \underline{AC} dom f = V$
31	27 30	eleqtrrid	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to ⋃_{k \in dom f} s (k) \in \underline{AC} dom f$
32	11 14 17 25 31	ptclsg	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to cls (\prod_{𝑡} ((k \in dom f ⟼ f (k)))) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))$
33	10 32	eqtrd	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))$
34	5 33	sylan2b	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k)) \to cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))$
35	34	ralrimiva	$⊢ (CHOICE \land f : dom f ⟶ Top) \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))$
36	35	ex	$⊢ CHOICE \to (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)))$
37	36	alrimiv	$⊢ CHOICE \to \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)))$
38		vex	$⊢ g \in V$
39	38	dmex	$⊢ dom g \in V$
40	39	a1i	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to dom g \in V$
41		fvex	$⊢ g (x) \in V$
42	41	a1i	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to g (x) \in V$
43		simplrr	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to \emptyset \notin ran g$
44		df-nel	$⊢ \emptyset \notin ran g \leftrightarrow \neg \emptyset \in ran g$
45	43 44	sylib	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to \neg \emptyset \in ran g$
46		funforn	$⊢ Fun g \leftrightarrow g : dom g \underset{onto}{⟶} ran g$
47		fof	$⊢ g : dom g \underset{onto}{⟶} ran g \to g : dom g ⟶ ran g$
48	46 47	sylbi	$⊢ Fun g \to g : dom g ⟶ ran g$
49	48	ad2antrl	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to g : dom g ⟶ ran g$
50	49	ffvelrnda	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to g (x) \in ran g$
51		eleq1	$⊢ g (x) = \emptyset \to (g (x) \in ran g \leftrightarrow \emptyset \in ran g)$
52	50 51	syl5ibcom	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to (g (x) = \emptyset \to \emptyset \in ran g)$
53	52	necon3bd	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to (\neg \emptyset \in ran g \to g (x) \neq \emptyset)$
54	45 53	mpd	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to g (x) \neq \emptyset$
55		eqid	$⊢ 𝒫 ⋃ g (x) = 𝒫 ⋃ g (x)$
56		eqid	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} = \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}$
57		eqid	$⊢ \prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})) = \prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))$
58		fveq1	$⊢ s = g \to s (k) = g (k)$
59	58	ixpeq2dv	$⊢ s = g \to \underset{k \in dom g}{⨉} s (k) = \underset{k \in dom g}{⨉} g (k)$
60		fveq2	$⊢ k = x \to g (k) = g (x)$
61	60	cbvixpv	$⊢ \underset{k \in dom g}{⨉} g (k) = \underset{x \in dom g}{⨉} g (x)$
62	59 61	eqtrdi	$⊢ s = g \to \underset{k \in dom g}{⨉} s (k) = \underset{x \in dom g}{⨉} g (x)$
63	62	fveq2d	$⊢ s = g \to cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{x \in dom g}{⨉} g (x))$
64	58	fveq2d	$⊢ s = g \to cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)) = cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (g (k))$
65	64	ixpeq2dv	$⊢ s = g \to \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (g (k))$
66	60	unieqd	$⊢ k = x \to ⋃ g (k) = ⋃ g (x)$
67	66	pweqd	$⊢ k = x \to 𝒫 ⋃ g (k) = 𝒫 ⋃ g (x)$
68	67	sneqd	$⊢ k = x \to \{𝒫 ⋃ g (k)\} = \{𝒫 ⋃ g (x)\}$
69	60 68	uneq12d	$⊢ k = x \to g (k) \cup \{𝒫 ⋃ g (k)\} = g (x) \cup \{𝒫 ⋃ g (x)\}$
70	69	pweqd	$⊢ k = x \to 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) = 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\})$
71	67	eleq1d	$⊢ k = x \to (𝒫 ⋃ g (k) \in y \leftrightarrow 𝒫 ⋃ g (x) \in y)$
72	69	eqeq2d	$⊢ k = x \to (y = g (k) \cup \{𝒫 ⋃ g (k)\} \leftrightarrow y = g (x) \cup \{𝒫 ⋃ g (x)\})$
73	71 72	imbi12d	$⊢ k = x \to ((𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\}) \leftrightarrow (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\}))$
74	70 73	rabeqbidv	$⊢ k = x \to \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\} = \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}$
75	74	fveq2d	$⊢ k = x \to cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) = cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})$
76	75 60	fveq12d	$⊢ k = x \to cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (g (k)) = cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (g (x))$
77	76	cbvixpv	$⊢ \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (g (k)) = \underset{x \in dom g}{⨉} cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (g (x))$
78	65 77	eqtrdi	$⊢ s = g \to \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)) = \underset{x \in dom g}{⨉} cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (g (x))$
79	63 78	eqeq12d	$⊢ s = g \to (cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)) \leftrightarrow cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{x \in dom g}{⨉} g (x)) = \underset{x \in dom g}{⨉} cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (g (x)))$
80		simpl	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)))$
81		snex	$⊢ \{𝒫 ⋃ g (x)\} \in V$
82	41 81	unex	$⊢ g (x) \cup \{𝒫 ⋃ g (x)\} \in V$
83		ssun2	$⊢ \{𝒫 ⋃ g (x)\} \subseteq g (x) \cup \{𝒫 ⋃ g (x)\}$
84	41	uniex	$⊢ ⋃ g (x) \in V$
85	84	pwex	$⊢ 𝒫 ⋃ g (x) \in V$
86	85	snid	$⊢ 𝒫 ⋃ g (x) \in \{𝒫 ⋃ g (x)\}$
87	83 86	sselii	$⊢ 𝒫 ⋃ g (x) \in (g (x) \cup \{𝒫 ⋃ g (x)\})$
88		epttop	$⊢ (g (x) \cup \{𝒫 ⋃ g (x)\} \in V \land 𝒫 ⋃ g (x) \in (g (x) \cup \{𝒫 ⋃ g (x)\})) \to \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in TopOn (g (x) \cup \{𝒫 ⋃ g (x)\})$
89	82 87 88	mp2an	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in TopOn (g (x) \cup \{𝒫 ⋃ g (x)\})$
90	89	topontopi	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in Top$
91	90	a1i	$⊢ ((\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \land x \in dom g) \to \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in Top$
92	91	fmpttd	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) : dom g ⟶ Top$
93	39	mptex	$⊢ (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \in V$
94		id	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})$
95		dmeq	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to dom f = dom (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})$
96	82	pwex	$⊢ 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \in V$
97	96	rabex	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in V$
98		eqid	$⊢ (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})$
99	97 98	dmmpti	$⊢ dom (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) = dom g$
100	95 99	eqtrdi	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to dom f = dom g$
101	94 100	feq12d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to (f : dom f ⟶ Top \leftrightarrow (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) : dom g ⟶ Top)$
102	100	ixpeq1d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) = \underset{k \in dom g}{⨉} 𝒫 ⋃ f (k)$
103		fveq1	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to f (k) = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (k)$
104		fveq2	$⊢ x = k \to g (x) = g (k)$
105	104	unieqd	$⊢ x = k \to ⋃ g (x) = ⋃ g (k)$
106	105	pweqd	$⊢ x = k \to 𝒫 ⋃ g (x) = 𝒫 ⋃ g (k)$
107	106	sneqd	$⊢ x = k \to \{𝒫 ⋃ g (x)\} = \{𝒫 ⋃ g (k)\}$
108	104 107	uneq12d	$⊢ x = k \to g (x) \cup \{𝒫 ⋃ g (x)\} = g (k) \cup \{𝒫 ⋃ g (k)\}$
109	108	pweqd	$⊢ x = k \to 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) = 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
110	106	eleq1d	$⊢ x = k \to (𝒫 ⋃ g (x) \in y \leftrightarrow 𝒫 ⋃ g (k) \in y)$
111	108	eqeq2d	$⊢ x = k \to (y = g (x) \cup \{𝒫 ⋃ g (x)\} \leftrightarrow y = g (k) \cup \{𝒫 ⋃ g (k)\})$
112	110 111	imbi12d	$⊢ x = k \to ((𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\}) \leftrightarrow (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\}))$
113	109 112	rabeqbidv	$⊢ x = k \to \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} = \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
114		fvex	$⊢ g (k) \in V$
115		snex	$⊢ \{𝒫 ⋃ g (k)\} \in V$
116	114 115	unex	$⊢ g (k) \cup \{𝒫 ⋃ g (k)\} \in V$
117	116	pwex	$⊢ 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \in V$
118	117	rabex	$⊢ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\} \in V$
119	113 98 118	fvmpt	$⊢ k \in dom g \to (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (k) = \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
120	103 119	sylan9eq	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to f (k) = \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
121	120	unieqd	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to ⋃ f (k) = ⋃ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
122		ssun2	$⊢ \{𝒫 ⋃ g (k)\} \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
123	114	uniex	$⊢ ⋃ g (k) \in V$
124	123	pwex	$⊢ 𝒫 ⋃ g (k) \in V$
125	124	snid	$⊢ 𝒫 ⋃ g (k) \in \{𝒫 ⋃ g (k)\}$
126	122 125	sselii	$⊢ 𝒫 ⋃ g (k) \in (g (k) \cup \{𝒫 ⋃ g (k)\})$
127		epttop	$⊢ (g (k) \cup \{𝒫 ⋃ g (k)\} \in V \land 𝒫 ⋃ g (k) \in (g (k) \cup \{𝒫 ⋃ g (k)\})) \to \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\} \in TopOn (g (k) \cup \{𝒫 ⋃ g (k)\})$
128	116 126 127	mp2an	$⊢ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\} \in TopOn (g (k) \cup \{𝒫 ⋃ g (k)\})$
129	128	toponunii	$⊢ g (k) \cup \{𝒫 ⋃ g (k)\} = ⋃ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
130	121 129	eqtr4di	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to ⋃ f (k) = g (k) \cup \{𝒫 ⋃ g (k)\}$
131	130	pweqd	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to 𝒫 ⋃ f (k) = 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
132	131	ixpeq2dva	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom g}{⨉} 𝒫 ⋃ f (k) = \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
133	102 132	eqtrd	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) = \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
134		2fveq3	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to cls (\prod_{𝑡} (f)) = cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\})))$
135	100	ixpeq1d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom f}{⨉} s (k) = \underset{k \in dom g}{⨉} s (k)$
136	134 135	fveq12d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k))$
137	100	ixpeq1d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom f}{⨉} cls (f (k)) (s (k)) = \underset{k \in dom g}{⨉} cls (f (k)) (s (k))$
138	120	fveq2d	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to cls (f (k)) = cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\})$
139	138	fveq1d	$⊢ (f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \land k \in dom g) \to cls (f (k)) (s (k)) = cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k))$
140	139	ixpeq2dva	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom g}{⨉} cls (f (k)) (s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k))$
141	137 140	eqtrd	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to \underset{k \in dom f}{⨉} cls (f (k)) (s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k))$
142	136 141	eqeq12d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to (cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)) \leftrightarrow cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)))$
143	133 142	raleqbidv	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to (\forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)) \leftrightarrow \forall s \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)))$
144	101 143	imbi12d	$⊢ f = (x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) \to ((f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \leftrightarrow ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) : dom g ⟶ Top \to \forall s \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k))))$
145	93 144	spcv	$⊢ \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \to ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) : dom g ⟶ Top \to \forall s \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k)))$
146	80 92 145	sylc	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to \forall s \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{k \in dom g}{⨉} s (k)) = \underset{k \in dom g}{⨉} cls (\{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}) (s (k))$
147		simprl	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to Fun g$
148	147	funfnd	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to g Fn dom g$
149		ssun1	$⊢ g (k) \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
150	114	elpw	$⊢ g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \leftrightarrow g (k) \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
151	149 150	mpbir	$⊢ g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
152	151	rgenw	$⊢ \forall k \in dom g g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
153	38	elixp	$⊢ g \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \leftrightarrow (g Fn dom g \land \forall k \in dom g g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}))$
154	148 152 153	sylanblrc	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to g \in \underset{k \in dom g}{⨉} 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
155	79 146 154	rspcdva	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to cls (\prod_{𝑡} ((x \in dom g ⟼ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}))) (\underset{x \in dom g}{⨉} g (x)) = \underset{x \in dom g}{⨉} cls (\{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\}) (g (x))$
156	40 42 54 55 56 57 155	dfac14lem	$⊢ (\forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \land (Fun g \land \emptyset \notin ran g)) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset$
157	156	ex	$⊢ \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \to ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
158	157	alrimiv	$⊢ \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \to \forall g ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
159		dfac9	$⊢ CHOICE \leftrightarrow \forall g ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
160	158 159	sylibr	$⊢ \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k))) \to CHOICE$
161	37 160	impbii	$⊢ CHOICE \leftrightarrow \forall f (f : dom f ⟶ Top \to \forall s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) cls (\prod_{𝑡} (f)) (\underset{k \in dom f}{⨉} s (k)) = \underset{k \in dom f}{⨉} cls (f (k)) (s (k)))$

Metamath Proof Explorer

Theorem dfac14

Proof