dcomex

Description: The Axiom of Dependent Choice implies Infinity, the way we have stated it. Thus, we haveInf+AC impliesDC andDC impliesInf, but AC does not implyInf. (Contributed by Mario Carneiro, 25-Jan-2013)

		Ref	Expression
	Assertion	dcomex	$⊢ ω \in V$

Proof

Step	Hyp	Ref	Expression
1		1n0	$⊢ 1_{𝑜} \neq \emptyset$
2		df-br	$⊢ f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \leftrightarrow ⟨f (n), f (suc n)⟩ \in \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
3		elsni	$⊢ ⟨f (n), f (suc n)⟩ \in \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to ⟨f (n), f (suc n)⟩ = ⟨1_{𝑜}, 1_{𝑜}⟩$
4		fvex	$⊢ f (n) \in V$
5		fvex	$⊢ f (suc n) \in V$
6	4 5	opth1	$⊢ ⟨f (n), f (suc n)⟩ = ⟨1_{𝑜}, 1_{𝑜}⟩ \to f (n) = 1_{𝑜}$
7	3 6	syl	$⊢ ⟨f (n), f (suc n)⟩ \in \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to f (n) = 1_{𝑜}$
8	2 7	sylbi	$⊢ f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to f (n) = 1_{𝑜}$
9		tz6.12i	$⊢ 1_{𝑜} \neq \emptyset \to (f (n) = 1_{𝑜} \to n f 1_{𝑜})$
10	1 8 9	mpsyl	$⊢ f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to n f 1_{𝑜}$
11		vex	$⊢ n \in V$
12		1oex	$⊢ 1_{𝑜} \in V$
13	11 12	breldm	$⊢ n f 1_{𝑜} \to n \in dom f$
14	10 13	syl	$⊢ f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to n \in dom f$
15	14	ralimi	$⊢ \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to \forall n \in ω n \in dom f$
16		dfss3	$⊢ ω \subseteq dom f \leftrightarrow \forall n \in ω n \in dom f$
17	15 16	sylibr	$⊢ \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to ω \subseteq dom f$
18		vex	$⊢ f \in V$
19	18	dmex	$⊢ dom f \in V$
20	19	ssex	$⊢ ω \subseteq dom f \to ω \in V$
21	17 20	syl	$⊢ \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n) \to ω \in V$
22		snex	$⊢ \{⟨1_{𝑜}, 1_{𝑜}⟩\} \in V$
23	12 12	fvsn	$⊢ \{⟨1_{𝑜}, 1_{𝑜}⟩\} (1_{𝑜}) = 1_{𝑜}$
24	12 12	funsn	$⊢ Fun \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
25	12	snid	$⊢ 1_{𝑜} \in \{1_{𝑜}\}$
26	12	dmsnop	$⊢ dom \{⟨1_{𝑜}, 1_{𝑜}⟩\} = \{1_{𝑜}\}$
27	25 26	eleqtrri	$⊢ 1_{𝑜} \in dom \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
28		funbrfvb	$⊢ (Fun \{⟨1_{𝑜}, 1_{𝑜}⟩\} \land 1_{𝑜} \in dom \{⟨1_{𝑜}, 1_{𝑜}⟩\}) \to (\{⟨1_{𝑜}, 1_{𝑜}⟩\} (1_{𝑜}) = 1_{𝑜} \leftrightarrow 1_{𝑜} \{⟨1_{𝑜}, 1_{𝑜}⟩\} 1_{𝑜})$
29	24 27 28	mp2an	$⊢ \{⟨1_{𝑜}, 1_{𝑜}⟩\} (1_{𝑜}) = 1_{𝑜} \leftrightarrow 1_{𝑜} \{⟨1_{𝑜}, 1_{𝑜}⟩\} 1_{𝑜}$
30	23 29	mpbi	$⊢ 1_{𝑜} \{⟨1_{𝑜}, 1_{𝑜}⟩\} 1_{𝑜}$
31		breq12	$⊢ (s = 1_{𝑜} \land t = 1_{𝑜}) \to (s \{⟨1_{𝑜}, 1_{𝑜}⟩\} t \leftrightarrow 1_{𝑜} \{⟨1_{𝑜}, 1_{𝑜}⟩\} 1_{𝑜})$
32	12 12 31	spc2ev	$⊢ 1_{𝑜} \{⟨1_{𝑜}, 1_{𝑜}⟩\} 1_{𝑜} \to \exists s \exists t s \{⟨1_{𝑜}, 1_{𝑜}⟩\} t$
33	30 32	ax-mp	$⊢ \exists s \exists t s \{⟨1_{𝑜}, 1_{𝑜}⟩\} t$
34		breq	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (s x t \leftrightarrow s \{⟨1_{𝑜}, 1_{𝑜}⟩\} t)$
35	34	2exbidv	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (\exists s \exists t s x t \leftrightarrow \exists s \exists t s \{⟨1_{𝑜}, 1_{𝑜}⟩\} t)$
36	33 35	mpbiri	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to \exists s \exists t s x t$
37		ssid	$⊢ \{1_{𝑜}\} \subseteq \{1_{𝑜}\}$
38	12	rnsnop	$⊢ ran \{⟨1_{𝑜}, 1_{𝑜}⟩\} = \{1_{𝑜}\}$
39	37 38 26	3sstr4i	$⊢ ran \{⟨1_{𝑜}, 1_{𝑜}⟩\} \subseteq dom \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
40		rneq	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to ran x = ran \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
41		dmeq	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to dom x = dom \{⟨1_{𝑜}, 1_{𝑜}⟩\}$
42	40 41	sseq12d	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (ran x \subseteq dom x \leftrightarrow ran \{⟨1_{𝑜}, 1_{𝑜}⟩\} \subseteq dom \{⟨1_{𝑜}, 1_{𝑜}⟩\})$
43	39 42	mpbiri	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to ran x \subseteq dom x$
44		pm5.5	$⊢ (\exists s \exists t s x t \land ran x \subseteq dom x) \to (((\exists s \exists t s x t \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)) \leftrightarrow \exists f \forall n \in ω f (n) x f (suc n))$
45	36 43 44	syl2anc	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (((\exists s \exists t s x t \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)) \leftrightarrow \exists f \forall n \in ω f (n) x f (suc n))$
46		breq	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (f (n) x f (suc n) \leftrightarrow f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n))$
47	46	ralbidv	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (\forall n \in ω f (n) x f (suc n) \leftrightarrow \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n))$
48	47	exbidv	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (\exists f \forall n \in ω f (n) x f (suc n) \leftrightarrow \exists f \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n))$
49	45 48	bitrd	$⊢ x = \{⟨1_{𝑜}, 1_{𝑜}⟩\} \to (((\exists s \exists t s x t \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)) \leftrightarrow \exists f \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n))$
50		ax-dc	$⊢ (\exists s \exists t s x t \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)$
51	22 49 50	vtocl	$⊢ \exists f \forall n \in ω f (n) \{⟨1_{𝑜}, 1_{𝑜}⟩\} f (suc n)$
52	21 51	exlimiiv	$⊢ ω \in V$

Metamath Proof Explorer

Theorem dcomex

Proof