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