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	ffvelcdmda	$⊢ (((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	5	bilanri	$⊢ ((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)$
19		vex	$⊢ s \in V$
20	19	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))$
21	20	simprbi	$⊢ s \in \underset{k \in dom f}{⨉} 𝒫 ⋃ f (k) \to \forall k \in dom f s (k) \in 𝒫 ⋃ f (k)$
22	18 21	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)$
23	22	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)$
24	23	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)$
25		fvex	$⊢ s (k) \in V$
26	13 25	iunex	$⊢ ⋃_{k \in dom f} s (k) \in V$
27		simpll	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to CHOICE$
28		acacni	$⊢ (CHOICE \land dom f \in V) \to \underline{AC} dom f = V$
29	27 13 28	sylancl	$⊢ ((CHOICE \land f : dom f ⟶ Top) \land s \in \underset{x \in dom f}{⨉} 𝒫 ⋃ f (x)) \to \underline{AC} dom f = V$
30	26 29	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$
31	11 14 17 24 30	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))$
32	10 31	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))$
33	5 32	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))$
34	33	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))$
35	34	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)))$
36	35	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)))$
37		vex	$⊢ g \in V$
38	37	dmex	$⊢ dom g \in V$
39	38	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$
40		fvex	$⊢ g (x) \in V$
41	40	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$
42		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$
43		df-nel	$⊢ \emptyset \notin ran g \leftrightarrow \neg \emptyset \in ran g$
44	42 43	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$
45		funforn	$⊢ Fun g \leftrightarrow g : dom g \underset{onto}{⟶} ran g$
46		fof	$⊢ g : dom g \underset{onto}{⟶} ran g \to g : dom g ⟶ ran g$
47	45 46	sylbi	$⊢ Fun g \to g : dom g ⟶ ran g$
48	47	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$
49	48	ffvelcdmda	$⊢ ((\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$
50		eleq1	$⊢ g (x) = \emptyset \to (g (x) \in ran g \leftrightarrow \emptyset \in ran g)$
51	49 50	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)$
52	51	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)$
53	44 52	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$
54		eqid	$⊢ 𝒫 ⋃ g (x) = 𝒫 ⋃ g (x)$
55		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)\})\}$
56		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)\})\}))$
57		fveq1	$⊢ s = g \to s (k) = g (k)$
58	57	ixpeq2dv	$⊢ s = g \to \underset{k \in dom g}{⨉} s (k) = \underset{k \in dom g}{⨉} g (k)$
59		fveq2	$⊢ k = x \to g (k) = g (x)$
60	59	cbvixpv	$⊢ \underset{k \in dom g}{⨉} g (k) = \underset{x \in dom g}{⨉} g (x)$
61	58 60	eqtrdi	$⊢ s = g \to \underset{k \in dom g}{⨉} s (k) = \underset{x \in dom g}{⨉} g (x)$
62	61	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))$
63	57	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))$
64	63	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))$
65	59	unieqd	$⊢ k = x \to ⋃ g (k) = ⋃ g (x)$
66	65	pweqd	$⊢ k = x \to 𝒫 ⋃ g (k) = 𝒫 ⋃ g (x)$
67	66	sneqd	$⊢ k = x \to \{𝒫 ⋃ g (k)\} = \{𝒫 ⋃ g (x)\}$
68	59 67	uneq12d	$⊢ k = x \to g (k) \cup \{𝒫 ⋃ g (k)\} = g (x) \cup \{𝒫 ⋃ g (x)\}$
69	68	pweqd	$⊢ k = x \to 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) = 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\})$
70	66	eleq1d	$⊢ k = x \to (𝒫 ⋃ g (k) \in y \leftrightarrow 𝒫 ⋃ g (x) \in y)$
71	68	eqeq2d	$⊢ k = x \to (y = g (k) \cup \{𝒫 ⋃ g (k)\} \leftrightarrow y = g (x) \cup \{𝒫 ⋃ g (x)\})$
72	70 71	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)\}))$
73	69 72	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)\})\}$
74	73	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)\})\})$
75	74 59	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))$
76	75	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))$
77	64 76	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))$
78	62 77	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)))$
79		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)))$
80		snex	$⊢ \{𝒫 ⋃ g (x)\} \in V$
81	40 80	unex	$⊢ g (x) \cup \{𝒫 ⋃ g (x)\} \in V$
82		ssun2	$⊢ \{𝒫 ⋃ g (x)\} \subseteq g (x) \cup \{𝒫 ⋃ g (x)\}$
83	40	uniex	$⊢ ⋃ g (x) \in V$
84	83	pwex	$⊢ 𝒫 ⋃ g (x) \in V$
85	84	snid	$⊢ 𝒫 ⋃ g (x) \in \{𝒫 ⋃ g (x)\}$
86	82 85	sselii	$⊢ 𝒫 ⋃ g (x) \in (g (x) \cup \{𝒫 ⋃ g (x)\})$
87		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)\})$
88	81 86 87	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)\})$
89	88	topontopi	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in Top$
90	89	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$
91	90	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$
92	38	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$
93		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)\})\})$
94		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)\})\})$
95	81	pwex	$⊢ 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \in V$
96	95	rabex	$⊢ \{y \in 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) \| (𝒫 ⋃ g (x) \in y \to y = g (x) \cup \{𝒫 ⋃ g (x)\})\} \in V$
97		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)\})\})$
98	96 97	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$
99	94 98	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$
100	93 99	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)$
101	99	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)$
102		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)$
103		fveq2	$⊢ x = k \to g (x) = g (k)$
104	103	unieqd	$⊢ x = k \to ⋃ g (x) = ⋃ g (k)$
105	104	pweqd	$⊢ x = k \to 𝒫 ⋃ g (x) = 𝒫 ⋃ g (k)$
106	105	sneqd	$⊢ x = k \to \{𝒫 ⋃ g (x)\} = \{𝒫 ⋃ g (k)\}$
107	103 106	uneq12d	$⊢ x = k \to g (x) \cup \{𝒫 ⋃ g (x)\} = g (k) \cup \{𝒫 ⋃ g (k)\}$
108	107	pweqd	$⊢ x = k \to 𝒫 (g (x) \cup \{𝒫 ⋃ g (x)\}) = 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
109	105	eleq1d	$⊢ x = k \to (𝒫 ⋃ g (x) \in y \leftrightarrow 𝒫 ⋃ g (k) \in y)$
110	107	eqeq2d	$⊢ x = k \to (y = g (x) \cup \{𝒫 ⋃ g (x)\} \leftrightarrow y = g (k) \cup \{𝒫 ⋃ g (k)\})$
111	109 110	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)\}))$
112	108 111	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)\})\}$
113		fvex	$⊢ g (k) \in V$
114		snex	$⊢ \{𝒫 ⋃ g (k)\} \in V$
115	113 114	unex	$⊢ g (k) \cup \{𝒫 ⋃ g (k)\} \in V$
116	115	pwex	$⊢ 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \in V$
117	116	rabex	$⊢ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\} \in V$
118	112 97 117	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)\})\}$
119	102 118	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)\})\}$
120	119	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)\})\}$
121		ssun2	$⊢ \{𝒫 ⋃ g (k)\} \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
122	113	uniex	$⊢ ⋃ g (k) \in V$
123	122	pwex	$⊢ 𝒫 ⋃ g (k) \in V$
124	123	snid	$⊢ 𝒫 ⋃ g (k) \in \{𝒫 ⋃ g (k)\}$
125	121 124	sselii	$⊢ 𝒫 ⋃ g (k) \in (g (k) \cup \{𝒫 ⋃ g (k)\})$
126		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)\})$
127	115 125 126	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)\})$
128	127	toponunii	$⊢ g (k) \cup \{𝒫 ⋃ g (k)\} = ⋃ \{y \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \| (𝒫 ⋃ g (k) \in y \to y = g (k) \cup \{𝒫 ⋃ g (k)\})\}$
129	120 128	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)\}$
130	129	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)\})$
131	130	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)\})$
132	101 131	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)\})$
133		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)\})\})))$
134	99	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)$
135	133 134	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))$
136	99	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))$
137	119	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)\})\})$
138	137	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))$
139	138	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))$
140	136 139	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))$
141	135 140	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)))$
142	132 141	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)))$
143	100 142	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))))$
144	92 143	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)))$
145	79 91 144	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))$
146		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$
147	146	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$
148		ssun1	$⊢ g (k) \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
149	113	elpw	$⊢ g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\}) \leftrightarrow g (k) \subseteq g (k) \cup \{𝒫 ⋃ g (k)\}$
150	148 149	mpbir	$⊢ g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
151	150	rgenw	$⊢ \forall k \in dom g g (k) \in 𝒫 (g (k) \cup \{𝒫 ⋃ g (k)\})$
152	37	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)\}))$
153	147 151 152	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)\})$
154	78 145 153	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))$
155	39 41 53 54 55 56 154	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$
156	155	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)$
157	156	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)$
158		dfac9	$⊢ CHOICE \leftrightarrow \forall g ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
159	157 158	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$
160	36 159	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