axdc2lem

Description: Lemma for axdc2 . We construct a relation R based on F such that x R y iff y e. ( Fx ) , and show that the "function" described by ax-dc can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	axdc2lem.1	$⊢ A \in V$
	axdc2lem.2	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
	axdc2lem.3	$⊢ G = (x \in ω ⟼ h (x))$
Assertion	axdc2lem	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k)))$

Proof

Step	Hyp	Ref	Expression
1		axdc2lem.1	$⊢ A \in V$
2		axdc2lem.2	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
3		axdc2lem.3	$⊢ G = (x \in ω ⟼ h (x))$
4	2	dmeqi	$⊢ dom R = dom \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
5		19.42v	$⊢ \exists y (x \in A \land y \in F (x)) \leftrightarrow (x \in A \land \exists y y \in F (x))$
6	5	abbii	$⊢ \{x \| \exists y (x \in A \land y \in F (x))\} = \{x \| (x \in A \land \exists y y \in F (x))\}$
7		dmopab	$⊢ dom \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} = \{x \| \exists y (x \in A \land y \in F (x))\}$
8		df-rab	$⊢ \{x \in A \| \exists y y \in F (x)\} = \{x \| (x \in A \land \exists y y \in F (x))\}$
9	6 7 8	3eqtr4i	$⊢ dom \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} = \{x \in A \| \exists y y \in F (x)\}$
10	4 9	eqtri	$⊢ dom R = \{x \in A \| \exists y y \in F (x)\}$
11		ffvelcdm	$⊢ (F : A ⟶ 𝒫 A ∖ \{\emptyset\} \land x \in A) \to F (x) \in (𝒫 A ∖ \{\emptyset\})$
12		eldifsni	$⊢ F (x) \in (𝒫 A ∖ \{\emptyset\}) \to F (x) \neq \emptyset$
13		n0	$⊢ F (x) \neq \emptyset \leftrightarrow \exists y y \in F (x)$
14	12 13	sylib	$⊢ F (x) \in (𝒫 A ∖ \{\emptyset\}) \to \exists y y \in F (x)$
15	11 14	syl	$⊢ (F : A ⟶ 𝒫 A ∖ \{\emptyset\} \land x \in A) \to \exists y y \in F (x)$
16	15	ralrimiva	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to \forall x \in A \exists y y \in F (x)$
17		rabid2	$⊢ A = \{x \in A \| \exists y y \in F (x)\} \leftrightarrow \forall x \in A \exists y y \in F (x)$
18	16 17	sylibr	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to A = \{x \in A \| \exists y y \in F (x)\}$
19	10 18	eqtr4id	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to dom R = A$
20	19	neeq1d	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to (dom R \neq \emptyset \leftrightarrow A \neq \emptyset)$
21	20	biimparc	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to dom R \neq \emptyset$
22		eldifi	$⊢ F (x) \in (𝒫 A ∖ \{\emptyset\}) \to F (x) \in 𝒫 A$
23		elelpwi	$⊢ (y \in F (x) \land F (x) \in 𝒫 A) \to y \in A$
24	23	expcom	$⊢ F (x) \in 𝒫 A \to (y \in F (x) \to y \in A)$
25	11 22 24	3syl	$⊢ (F : A ⟶ 𝒫 A ∖ \{\emptyset\} \land x \in A) \to (y \in F (x) \to y \in A)$
26	25	expimpd	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to ((x \in A \land y \in F (x)) \to y \in A)$
27	26	exlimdv	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to (\exists x (x \in A \land y \in F (x)) \to y \in A)$
28	27	alrimiv	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to \forall y (\exists x (x \in A \land y \in F (x)) \to y \in A)$
29	2	rneqi	$⊢ ran R = ran \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
30		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} = \{y \| \exists x (x \in A \land y \in F (x))\}$
31	29 30	eqtri	$⊢ ran R = \{y \| \exists x (x \in A \land y \in F (x))\}$
32	31	sseq1i	$⊢ ran R \subseteq A \leftrightarrow \{y \| \exists x (x \in A \land y \in F (x))\} \subseteq A$
33		abss	$⊢ \{y \| \exists x (x \in A \land y \in F (x))\} \subseteq A \leftrightarrow \forall y (\exists x (x \in A \land y \in F (x)) \to y \in A)$
34	32 33	bitri	$⊢ ran R \subseteq A \leftrightarrow \forall y (\exists x (x \in A \land y \in F (x)) \to y \in A)$
35	28 34	sylibr	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to ran R \subseteq A$
36	35 19	sseqtrrd	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to ran R \subseteq dom R$
37	36	adantl	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ran R \subseteq dom R$
38		fvrn0	$⊢ F (x) \in (ran F \cup \{\emptyset\})$
39		elssuni	$⊢ F (x) \in (ran F \cup \{\emptyset\}) \to F (x) \subseteq ⋃ (ran F \cup \{\emptyset\})$
40	38 39	ax-mp	$⊢ F (x) \subseteq ⋃ (ran F \cup \{\emptyset\})$
41	40	sseli	$⊢ y \in F (x) \to y \in ⋃ (ran F \cup \{\emptyset\})$
42	41	anim2i	$⊢ (x \in A \land y \in F (x)) \to (x \in A \land y \in ⋃ (ran F \cup \{\emptyset\}))$
43	42	ssopab2i	$⊢ \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \subseteq \{⟨x, y⟩ \| (x \in A \land y \in ⋃ (ran F \cup \{\emptyset\}))\}$
44		df-xp	$⊢ A \times ⋃ (ran F \cup \{\emptyset\}) = \{⟨x, y⟩ \| (x \in A \land y \in ⋃ (ran F \cup \{\emptyset\}))\}$
45	43 2 44	3sstr4i	$⊢ R \subseteq A \times ⋃ (ran F \cup \{\emptyset\})$
46		frn	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to ran F \subseteq 𝒫 A ∖ \{\emptyset\}$
47	46	adantl	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ran F \subseteq 𝒫 A ∖ \{\emptyset\}$
48	1	pwex	$⊢ 𝒫 A \in V$
49	48	difexi	$⊢ 𝒫 A ∖ \{\emptyset\} \in V$
50	49	ssex	$⊢ ran F \subseteq 𝒫 A ∖ \{\emptyset\} \to ran F \in V$
51	47 50	syl	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ran F \in V$
52		p0ex	$⊢ \{\emptyset\} \in V$
53		unexg	$⊢ (ran F \in V \land \{\emptyset\} \in V) \to ran F \cup \{\emptyset\} \in V$
54	51 52 53	sylancl	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ran F \cup \{\emptyset\} \in V$
55	54	uniexd	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ⋃ (ran F \cup \{\emptyset\}) \in V$
56		xpexg	$⊢ (A \in V \land ⋃ (ran F \cup \{\emptyset\}) \in V) \to A \times ⋃ (ran F \cup \{\emptyset\}) \in V$
57	1 55 56	sylancr	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to A \times ⋃ (ran F \cup \{\emptyset\}) \in V$
58		ssexg	$⊢ (R \subseteq A \times ⋃ (ran F \cup \{\emptyset\}) \land A \times ⋃ (ran F \cup \{\emptyset\}) \in V) \to R \in V$
59	45 57 58	sylancr	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to R \in V$
60		n0	$⊢ dom r \neq \emptyset \leftrightarrow \exists x x \in dom r$
61		vex	$⊢ x \in V$
62	61	eldm	$⊢ x \in dom r \leftrightarrow \exists y x r y$
63	62	exbii	$⊢ \exists x x \in dom r \leftrightarrow \exists x \exists y x r y$
64	60 63	bitr2i	$⊢ \exists x \exists y x r y \leftrightarrow dom r \neq \emptyset$
65		dmeq	$⊢ r = R \to dom r = dom R$
66	65	neeq1d	$⊢ r = R \to (dom r \neq \emptyset \leftrightarrow dom R \neq \emptyset)$
67	64 66	bitrid	$⊢ r = R \to (\exists x \exists y x r y \leftrightarrow dom R \neq \emptyset)$
68		rneq	$⊢ r = R \to ran r = ran R$
69	68 65	sseq12d	$⊢ r = R \to (ran r \subseteq dom r \leftrightarrow ran R \subseteq dom R)$
70	67 69	anbi12d	$⊢ r = R \to ((\exists x \exists y x r y \land ran r \subseteq dom r) \leftrightarrow (dom R \neq \emptyset \land ran R \subseteq dom R))$
71		breq	$⊢ r = R \to (h (k) r h (suc k) \leftrightarrow h (k) R h (suc k))$
72	71	ralbidv	$⊢ r = R \to (\forall k \in ω h (k) r h (suc k) \leftrightarrow \forall k \in ω h (k) R h (suc k))$
73	72	exbidv	$⊢ r = R \to (\exists h \forall k \in ω h (k) r h (suc k) \leftrightarrow \exists h \forall k \in ω h (k) R h (suc k))$
74	70 73	imbi12d	$⊢ r = R \to (((\exists x \exists y x r y \land ran r \subseteq dom r) \to \exists h \forall k \in ω h (k) r h (suc k)) \leftrightarrow ((dom R \neq \emptyset \land ran R \subseteq dom R) \to \exists h \forall k \in ω h (k) R h (suc k)))$
75		ax-dc	$⊢ (\exists x \exists y x r y \land ran r \subseteq dom r) \to \exists h \forall k \in ω h (k) r h (suc k)$
76	74 75	vtoclg	$⊢ R \in V \to ((dom R \neq \emptyset \land ran R \subseteq dom R) \to \exists h \forall k \in ω h (k) R h (suc k))$
77	59 76	syl	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to ((dom R \neq \emptyset \land ran R \subseteq dom R) \to \exists h \forall k \in ω h (k) R h (suc k))$
78	21 37 77	mp2and	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists h \forall k \in ω h (k) R h (suc k)$
79		simpr	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to F : A ⟶ 𝒫 A ∖ \{\emptyset\}$
80		fveq2	$⊢ k = x \to h (k) = h (x)$
81		suceq	$⊢ k = x \to suc k = suc x$
82	81	fveq2d	$⊢ k = x \to h (suc k) = h (suc x)$
83	80 82	breq12d	$⊢ k = x \to (h (k) R h (suc k) \leftrightarrow h (x) R h (suc x))$
84	83	rspccv	$⊢ \forall k \in ω h (k) R h (suc k) \to (x \in ω \to h (x) R h (suc x))$
85		fvex	$⊢ h (x) \in V$
86		fvex	$⊢ h (suc x) \in V$
87	85 86	breldm	$⊢ h (x) R h (suc x) \to h (x) \in dom R$
88	84 87	syl6	$⊢ \forall k \in ω h (k) R h (suc k) \to (x \in ω \to h (x) \in dom R)$
89	88	imp	$⊢ (\forall k \in ω h (k) R h (suc k) \land x \in ω) \to h (x) \in dom R$
90	89	adantll	$⊢ ((dom R = A \land \forall k \in ω h (k) R h (suc k)) \land x \in ω) \to h (x) \in dom R$
91		eleq2	$⊢ dom R = A \to (h (x) \in dom R \leftrightarrow h (x) \in A)$
92	91	ad2antrr	$⊢ ((dom R = A \land \forall k \in ω h (k) R h (suc k)) \land x \in ω) \to (h (x) \in dom R \leftrightarrow h (x) \in A)$
93	90 92	mpbid	$⊢ ((dom R = A \land \forall k \in ω h (k) R h (suc k)) \land x \in ω) \to h (x) \in A$
94	93 3	fmptd	$⊢ (dom R = A \land \forall k \in ω h (k) R h (suc k)) \to G : ω ⟶ A$
95	94	ex	$⊢ dom R = A \to (\forall k \in ω h (k) R h (suc k) \to G : ω ⟶ A)$
96	19 95	syl	$⊢ F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to (\forall k \in ω h (k) R h (suc k) \to G : ω ⟶ A)$
97	96	impcom	$⊢ (\forall k \in ω h (k) R h (suc k) \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to G : ω ⟶ A$
98		fveq2	$⊢ x = k \to h (x) = h (k)$
99		fvex	$⊢ h (k) \in V$
100	98 3 99	fvmpt	$⊢ k \in ω \to G (k) = h (k)$
101		peano2	$⊢ k \in ω \to suc k \in ω$
102		fvex	$⊢ h (suc k) \in V$
103		fveq2	$⊢ x = suc k \to h (x) = h (suc k)$
104	103 3	fvmptg	$⊢ (suc k \in ω \land h (suc k) \in V) \to G (suc k) = h (suc k)$
105	101 102 104	sylancl	$⊢ k \in ω \to G (suc k) = h (suc k)$
106	100 105	breq12d	$⊢ k \in ω \to (G (k) R G (suc k) \leftrightarrow h (k) R h (suc k))$
107		fvex	$⊢ G (k) \in V$
108		fvex	$⊢ G (suc k) \in V$
109		eleq1	$⊢ x = G (k) \to (x \in A \leftrightarrow G (k) \in A)$
110		fveq2	$⊢ x = G (k) \to F (x) = F (G (k))$
111	110	eleq2d	$⊢ x = G (k) \to (y \in F (x) \leftrightarrow y \in F (G (k)))$
112	109 111	anbi12d	$⊢ x = G (k) \to ((x \in A \land y \in F (x)) \leftrightarrow (G (k) \in A \land y \in F (G (k))))$
113		eleq1	$⊢ y = G (suc k) \to (y \in F (G (k)) \leftrightarrow G (suc k) \in F (G (k)))$
114	113	anbi2d	$⊢ y = G (suc k) \to ((G (k) \in A \land y \in F (G (k))) \leftrightarrow (G (k) \in A \land G (suc k) \in F (G (k))))$
115	107 108 112 114 2	brab	$⊢ G (k) R G (suc k) \leftrightarrow (G (k) \in A \land G (suc k) \in F (G (k)))$
116	115	simprbi	$⊢ G (k) R G (suc k) \to G (suc k) \in F (G (k))$
117	106 116	biimtrrdi	$⊢ k \in ω \to (h (k) R h (suc k) \to G (suc k) \in F (G (k)))$
118	117	ralimia	$⊢ \forall k \in ω h (k) R h (suc k) \to \forall k \in ω G (suc k) \in F (G (k))$
119	118	adantr	$⊢ (\forall k \in ω h (k) R h (suc k) \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \forall k \in ω G (suc k) \in F (G (k))$
120		fvrn0	$⊢ h (x) \in (ran h \cup \{\emptyset\})$
121	120	rgenw	$⊢ \forall x \in ω h (x) \in (ran h \cup \{\emptyset\})$
122		eqid	$⊢ (x \in ω ⟼ h (x)) = (x \in ω ⟼ h (x))$
123	122	fmpt	$⊢ \forall x \in ω h (x) \in (ran h \cup \{\emptyset\}) \leftrightarrow (x \in ω ⟼ h (x)) : ω ⟶ ran h \cup \{\emptyset\}$
124	121 123	mpbi	$⊢ (x \in ω ⟼ h (x)) : ω ⟶ ran h \cup \{\emptyset\}$
125		dcomex	$⊢ ω \in V$
126		vex	$⊢ h \in V$
127	126	rnex	$⊢ ran h \in V$
128	127 52	unex	$⊢ ran h \cup \{\emptyset\} \in V$
129		fex2	$⊢ ((x \in ω ⟼ h (x)) : ω ⟶ ran h \cup \{\emptyset\} \land ω \in V \land ran h \cup \{\emptyset\} \in V) \to (x \in ω ⟼ h (x)) \in V$
130	124 125 128 129	mp3an	$⊢ (x \in ω ⟼ h (x)) \in V$
131	3 130	eqeltri	$⊢ G \in V$
132		feq1	$⊢ g = G \to (g : ω ⟶ A \leftrightarrow G : ω ⟶ A)$
133		fveq1	$⊢ g = G \to g (suc k) = G (suc k)$
134		fveq1	$⊢ g = G \to g (k) = G (k)$
135	134	fveq2d	$⊢ g = G \to F (g (k)) = F (G (k))$
136	133 135	eleq12d	$⊢ g = G \to (g (suc k) \in F (g (k)) \leftrightarrow G (suc k) \in F (G (k)))$
137	136	ralbidv	$⊢ g = G \to (\forall k \in ω g (suc k) \in F (g (k)) \leftrightarrow \forall k \in ω G (suc k) \in F (G (k)))$
138	132 137	anbi12d	$⊢ g = G \to ((g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k))) \leftrightarrow (G : ω ⟶ A \land \forall k \in ω G (suc k) \in F (G (k))))$
139	131 138	spcev	$⊢ (G : ω ⟶ A \land \forall k \in ω G (suc k) \in F (G (k))) \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k)))$
140	97 119 139	syl2anc	$⊢ (\forall k \in ω h (k) R h (suc k) \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k)))$
141	140	ex	$⊢ \forall k \in ω h (k) R h (suc k) \to (F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k))))$
142	141	exlimiv	$⊢ \exists h \forall k \in ω h (k) R h (suc k) \to (F : A ⟶ 𝒫 A ∖ \{\emptyset\} \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k))))$
143	78 79 142	sylc	$⊢ (A \neq \emptyset \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land \forall k \in ω g (suc k) \in F (g (k)))$

Metamath Proof Explorer

Theorem axdc2lem

Proof