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

Metamath Proof Explorer

Theorem dfac21

Proof