axdclem2

Description: Lemma for axdc . Using the full Axiom of Choice, we can construct a choice function g on ~P dom x . From this, we can build a sequence F starting at any value s e. dom x by repeatedly applying g to the set ( Fx ) (where x is the value from the previous iteration). (Contributed by Mario Carneiro, 25-Jan-2013)

		Ref	Expression
	Hypothesis	axdclem2.1	$⊢ F = {rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}$
	Assertion	axdclem2	$⊢ \exists z s x z \to (ran x \subseteq dom x \to \exists f \forall n \in ω f (n) x f (suc n))$

Proof

Step	Hyp	Ref	Expression
1		axdclem2.1	$⊢ F = {rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}$
2		frfnom	$⊢ ({rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}) Fn ω$
3	1	fneq1i	$⊢ F Fn ω \leftrightarrow ({rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}) Fn ω$
4	2 3	mpbir	$⊢ F Fn ω$
5	4	a1i	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to F Fn ω$
6		omex	$⊢ ω \in V$
7	6	a1i	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to ω \in V$
8	5 7	fnexd	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to F \in V$
9		fveq2	$⊢ n = \emptyset \to F (n) = F (\emptyset)$
10		suceq	$⊢ n = \emptyset \to suc n = suc \emptyset$
11	10	fveq2d	$⊢ n = \emptyset \to F (suc n) = F (suc \emptyset)$
12	9 11	breq12d	$⊢ n = \emptyset \to (F (n) x F (suc n) \leftrightarrow F (\emptyset) x F (suc \emptyset))$
13		fveq2	$⊢ n = k \to F (n) = F (k)$
14		suceq	$⊢ n = k \to suc n = suc k$
15	14	fveq2d	$⊢ n = k \to F (suc n) = F (suc k)$
16	13 15	breq12d	$⊢ n = k \to (F (n) x F (suc n) \leftrightarrow F (k) x F (suc k))$
17		fveq2	$⊢ n = suc k \to F (n) = F (suc k)$
18		suceq	$⊢ n = suc k \to suc n = suc suc k$
19	18	fveq2d	$⊢ n = suc k \to F (suc n) = F (suc suc k)$
20	17 19	breq12d	$⊢ n = suc k \to (F (n) x F (suc n) \leftrightarrow F (suc k) x F (suc suc k))$
21	1	fveq1i	$⊢ F (\emptyset) = ({rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}) (\emptyset)$
22		fr0g	$⊢ s \in V \to ({rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}) (\emptyset) = s$
23	22	elv	$⊢ ({rec ((y \in V ⟼ g (\{z \| y x z\})), s) ↾}_{ω}) (\emptyset) = s$
24	21 23	eqtri	$⊢ F (\emptyset) = s$
25	24	breq1i	$⊢ F (\emptyset) x z \leftrightarrow s x z$
26	25	biimpri	$⊢ s x z \to F (\emptyset) x z$
27	26	eximi	$⊢ \exists z s x z \to \exists z F (\emptyset) x z$
28		peano1	$⊢ \emptyset \in ω$
29	1	axdclem	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (\emptyset) x z) \to (\emptyset \in ω \to F (\emptyset) x F (suc \emptyset))$
30	28 29	mpi	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (\emptyset) x z) \to F (\emptyset) x F (suc \emptyset)$
31	27 30	syl3an3	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z s x z) \to F (\emptyset) x F (suc \emptyset)$
32	31	3com23	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to F (\emptyset) x F (suc \emptyset)$
33		fvex	$⊢ F (k) \in V$
34		fvex	$⊢ F (suc k) \in V$
35	33 34	brelrn	$⊢ F (k) x F (suc k) \to F (suc k) \in ran x$
36		ssel	$⊢ ran x \subseteq dom x \to (F (suc k) \in ran x \to F (suc k) \in dom x)$
37	35 36	syl5	$⊢ ran x \subseteq dom x \to (F (k) x F (suc k) \to F (suc k) \in dom x)$
38	34	eldm	$⊢ F (suc k) \in dom x \leftrightarrow \exists z F (suc k) x z$
39	37 38	imbitrdi	$⊢ ran x \subseteq dom x \to (F (k) x F (suc k) \to \exists z F (suc k) x z)$
40	39	ad2antll	$⊢ (k \in ω \land (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x)) \to (F (k) x F (suc k) \to \exists z F (suc k) x z)$
41		peano2	$⊢ k \in ω \to suc k \in ω$
42	1	axdclem	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (suc k) x z) \to (suc k \in ω \to F (suc k) x F (suc suc k))$
43	41 42	syl5	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x \land \exists z F (suc k) x z) \to (k \in ω \to F (suc k) x F (suc suc k))$
44	43	3expia	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x) \to (\exists z F (suc k) x z \to (k \in ω \to F (suc k) x F (suc suc k)))$
45	44	com3r	$⊢ k \in ω \to ((\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x) \to (\exists z F (suc k) x z \to F (suc k) x F (suc suc k)))$
46	45	imp	$⊢ (k \in ω \land (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x)) \to (\exists z F (suc k) x z \to F (suc k) x F (suc suc k))$
47	40 46	syld	$⊢ (k \in ω \land (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land ran x \subseteq dom x)) \to (F (k) x F (suc k) \to F (suc k) x F (suc suc k))$
48	47	3adantr2	$⊢ (k \in ω \land (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x)) \to (F (k) x F (suc k) \to F (suc k) x F (suc suc k))$
49	48	ex	$⊢ k \in ω \to ((\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to (F (k) x F (suc k) \to F (suc k) x F (suc suc k)))$
50	12 16 20 32 49	finds2	$⊢ n \in ω \to ((\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to F (n) x F (suc n))$
51	50	com12	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to (n \in ω \to F (n) x F (suc n))$
52	51	ralrimiv	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to \forall n \in ω F (n) x F (suc n)$
53		fveq1	$⊢ f = F \to f (n) = F (n)$
54		fveq1	$⊢ f = F \to f (suc n) = F (suc n)$
55	53 54	breq12d	$⊢ f = F \to (f (n) x f (suc n) \leftrightarrow F (n) x F (suc n))$
56	55	ralbidv	$⊢ f = F \to (\forall n \in ω f (n) x f (suc n) \leftrightarrow \forall n \in ω F (n) x F (suc n))$
57	8 52 56	spcedv	$⊢ (\forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \land \exists z s x z \land ran x \subseteq dom x) \to \exists f \forall n \in ω f (n) x f (suc n)$
58	57	3exp	$⊢ \forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y) \to (\exists z s x z \to (ran x \subseteq dom x \to \exists f \forall n \in ω f (n) x f (suc n)))$
59		vex	$⊢ x \in V$
60	59	dmex	$⊢ dom x \in V$
61	60	pwex	$⊢ 𝒫 dom x \in V$
62	61	ac4c	$⊢ \exists g \forall y \in 𝒫 dom x (y \neq \emptyset \to g (y) \in y)$
63	58 62	exlimiiv	$⊢ \exists z s x z \to (ran x \subseteq dom x \to \exists f \forall n \in ω f (n) x f (suc n))$

Metamath Proof Explorer

Theorem axdclem2

Proof