dfac21

Description: Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015) (Revised by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	dfac21	$⊢ CHOICE \leftrightarrow \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ f \in V$
2	1	dmex	$⊢ dom f \in V$
3	2	a1i	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to dom f \in V$
4		simpr	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to f : dom f ⟶ Comp$
5		fvex	$⊢ \prod_{𝑡} (f) \in V$
6	5	uniex	$⊢ ⋃ \prod_{𝑡} (f) \in V$
7		acufl	$⊢ CHOICE \to UFL = V$
8	7	adantr	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to UFL = V$
9	6 8	eleqtrrid	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to ⋃ \prod_{𝑡} (f) \in UFL$
10		simpl	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to CHOICE$
11		dfac10	$⊢ CHOICE \leftrightarrow dom card = V$
12	10 11	sylib	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to dom card = V$
13	6 12	eleqtrrid	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to ⋃ \prod_{𝑡} (f) \in dom card$
14	9 13	elind	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to ⋃ \prod_{𝑡} (f) \in (UFL \cap dom card)$
15		eqid	$⊢ \prod_{𝑡} (f) = \prod_{𝑡} (f)$
16		eqid	$⊢ ⋃ \prod_{𝑡} (f) = ⋃ \prod_{𝑡} (f)$
17	15 16	ptcmpg	$⊢ (dom f \in V \land f : dom f ⟶ Comp \land ⋃ \prod_{𝑡} (f) \in (UFL \cap dom card)) \to \prod_{𝑡} (f) \in Comp$
18	3 4 14 17	syl3anc	$⊢ (CHOICE \land f : dom f ⟶ Comp) \to \prod_{𝑡} (f) \in Comp$
19	18	ex	$⊢ CHOICE \to (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp)$
20	19	alrimiv	$⊢ CHOICE \to \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp)$
21		fvex	$⊢ g (y) \in V$
22		kelac2lem	$⊢ g (y) \in V \to topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}) \in Comp$
23	21 22	mp1i	$⊢ ((Fun g \land \emptyset \notin ran g) \land y \in dom g) \to topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}) \in Comp$
24	23	fmpttd	$⊢ (Fun g \land \emptyset \notin ran g) \to (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) : dom g ⟶ Comp$
25	24	ffdmd	$⊢ (Fun g \land \emptyset \notin ran g) \to (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) : dom (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) ⟶ Comp$
26		vex	$⊢ g \in V$
27	26	dmex	$⊢ dom g \in V$
28	27	mptex	$⊢ (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \in V$
29		id	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))$
30		dmeq	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to dom f = dom (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))$
31	29 30	feq12d	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to (f : dom f ⟶ Comp \leftrightarrow (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) : dom (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) ⟶ Comp)$
32		fveq2	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to \prod_{𝑡} (f) = \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})))$
33	32	eleq1d	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to (\prod_{𝑡} (f) \in Comp \leftrightarrow \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp)$
34	31 33	imbi12d	$⊢ f = (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) \to ((f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \leftrightarrow ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) : dom (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) ⟶ Comp \to \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp))$
35	28 34	spcv	$⊢ \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \to ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) : dom (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) ⟶ Comp \to \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp)$
36	25 35	syl5com	$⊢ (Fun g \land \emptyset \notin ran g) \to (\forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \to \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp)$
37		fvex	$⊢ g (x) \in V$
38	37	a1i	$⊢ (((Fun g \land \emptyset \notin ran g) \land \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp) \land x \in dom g) \to g (x) \in V$
39		df-nel	$⊢ \emptyset \notin ran g \leftrightarrow \neg \emptyset \in ran g$
40	39	biimpi	$⊢ \emptyset \notin ran g \to \neg \emptyset \in ran g$
41	40	ad2antlr	$⊢ ((Fun g \land \emptyset \notin ran g) \land x \in dom g) \to \neg \emptyset \in ran g$
42		fvelrn	$⊢ (Fun g \land x \in dom g) \to g (x) \in ran g$
43	42	adantlr	$⊢ ((Fun g \land \emptyset \notin ran g) \land x \in dom g) \to g (x) \in ran g$
44		eleq1	$⊢ g (x) = \emptyset \to (g (x) \in ran g \leftrightarrow \emptyset \in ran g)$
45	43 44	syl5ibcom	$⊢ ((Fun g \land \emptyset \notin ran g) \land x \in dom g) \to (g (x) = \emptyset \to \emptyset \in ran g)$
46	45	necon3bd	$⊢ ((Fun g \land \emptyset \notin ran g) \land x \in dom g) \to (\neg \emptyset \in ran g \to g (x) \neq \emptyset)$
47	41 46	mpd	$⊢ ((Fun g \land \emptyset \notin ran g) \land x \in dom g) \to g (x) \neq \emptyset$
48	47	adantlr	$⊢ (((Fun g \land \emptyset \notin ran g) \land \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp) \land x \in dom g) \to g (x) \neq \emptyset$
49		fveq2	$⊢ y = x \to g (y) = g (x)$
50	49	unieqd	$⊢ y = x \to ⋃ g (y) = ⋃ g (x)$
51	50	pweqd	$⊢ y = x \to 𝒫 ⋃ g (y) = 𝒫 ⋃ g (x)$
52	51	sneqd	$⊢ y = x \to \{𝒫 ⋃ g (y)\} = \{𝒫 ⋃ g (x)\}$
53	49 52	preq12d	$⊢ y = x \to \{g (y), \{𝒫 ⋃ g (y)\}\} = \{g (x), \{𝒫 ⋃ g (x)\}\}$
54	53	fveq2d	$⊢ y = x \to topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}) = topGen (\{g (x), \{𝒫 ⋃ g (x)\}\})$
55	54	cbvmptv	$⊢ (y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\})) = (x \in dom g ⟼ topGen (\{g (x), \{𝒫 ⋃ g (x)\}\}))$
56	55	fveq2i	$⊢ \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) = \prod_{𝑡} ((x \in dom g ⟼ topGen (\{g (x), \{𝒫 ⋃ g (x)\}\})))$
57	56	eleq1i	$⊢ \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp \leftrightarrow \prod_{𝑡} ((x \in dom g ⟼ topGen (\{g (x), \{𝒫 ⋃ g (x)\}\}))) \in Comp$
58	57	biimpi	$⊢ \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp \to \prod_{𝑡} ((x \in dom g ⟼ topGen (\{g (x), \{𝒫 ⋃ g (x)\}\}))) \in Comp$
59	58	adantl	$⊢ ((Fun g \land \emptyset \notin ran g) \land \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp) \to \prod_{𝑡} ((x \in dom g ⟼ topGen (\{g (x), \{𝒫 ⋃ g (x)\}\}))) \in Comp$
60	38 48 59	kelac2	$⊢ ((Fun g \land \emptyset \notin ran g) \land \prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset$
61	60	ex	$⊢ (Fun g \land \emptyset \notin ran g) \to (\prod_{𝑡} ((y \in dom g ⟼ topGen (\{g (y), \{𝒫 ⋃ g (y)\}\}))) \in Comp \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
62	36 61	syldc	$⊢ \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \to ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
63	62	alrimiv	$⊢ \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \to \forall g ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
64		dfac9	$⊢ CHOICE \leftrightarrow \forall g ((Fun g \land \emptyset \notin ran g) \to \underset{x \in dom g}{⨉} g (x) \neq \emptyset)$
65	63 64	sylibr	$⊢ \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp) \to CHOICE$
66	20 65	impbii	$⊢ CHOICE \leftrightarrow \forall f (f : dom f ⟶ Comp \to \prod_{𝑡} (f) \in Comp)$

Metamath Proof Explorer

Theorem dfac21

Proof