axdc4uzlem

	Ref	Expression
Hypotheses	axdc4uz.1	$⊢ M \in ℤ$
	axdc4uz.2	$⊢ Z = ℤ_{\geq M}$
	axdc4uz.3	$⊢ A \in V$
	axdc4uz.4	$⊢ G = {rec ((y \in V ⟼ y + 1), M) ↾}_{ω}$
	axdc4uz.5	$⊢ H = (n \in ω, x \in A ⟼ G (n) F x)$
Assertion	axdc4uzlem	$⊢ (C \in A \land F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k)))$

Proof

Step	Hyp	Ref	Expression
1		axdc4uz.1	$⊢ M \in ℤ$
2		axdc4uz.2	$⊢ Z = ℤ_{\geq M}$
3		axdc4uz.3	$⊢ A \in V$
4		axdc4uz.4	$⊢ G = {rec ((y \in V ⟼ y + 1), M) ↾}_{ω}$
5		axdc4uz.5	$⊢ H = (n \in ω, x \in A ⟼ G (n) F x)$
6	1 4	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq M}$
7		f1oeq3	$⊢ Z = ℤ_{\geq M} \to (G : ω \underset{1-1 onto}{⟶} Z \leftrightarrow G : ω \underset{1-1 onto}{⟶} ℤ_{\geq M})$
8	2 7	ax-mp	$⊢ G : ω \underset{1-1 onto}{⟶} Z \leftrightarrow G : ω \underset{1-1 onto}{⟶} ℤ_{\geq M}$
9	6 8	mpbir	$⊢ G : ω \underset{1-1 onto}{⟶} Z$
10		f1of	$⊢ G : ω \underset{1-1 onto}{⟶} Z \to G : ω ⟶ Z$
11	9 10	ax-mp	$⊢ G : ω ⟶ Z$
12	11	ffvelrni	$⊢ n \in ω \to G (n) \in Z$
13		fovrn	$⊢ (F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land G (n) \in Z \land x \in A) \to G (n) F x \in (𝒫 A ∖ \{\emptyset\})$
14	12 13	syl3an2	$⊢ (F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to G (n) F x \in (𝒫 A ∖ \{\emptyset\})$
15	14	3expb	$⊢ (F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land (n \in ω \land x \in A)) \to G (n) F x \in (𝒫 A ∖ \{\emptyset\})$
16	15	ralrimivva	$⊢ F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\} \to \forall n \in ω \forall x \in A G (n) F x \in (𝒫 A ∖ \{\emptyset\})$
17	5	fmpo	$⊢ \forall n \in ω \forall x \in A G (n) F x \in (𝒫 A ∖ \{\emptyset\}) \leftrightarrow H : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}$
18	16 17	sylib	$⊢ F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\} \to H : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}$
19	3	axdc4	$⊢ (C \in A \land H : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists f (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m)))$
20	18 19	sylan2	$⊢ (C \in A \land F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists f (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m)))$
21		f1ocnv	$⊢ G : ω \underset{1-1 onto}{⟶} Z \to G^{-1} : Z \underset{1-1 onto}{⟶} ω$
22		f1of	$⊢ G^{-1} : Z \underset{1-1 onto}{⟶} ω \to G^{-1} : Z ⟶ ω$
23	9 21 22	mp2b	$⊢ G^{-1} : Z ⟶ ω$
24		fco	$⊢ (f : ω ⟶ A \land G^{-1} : Z ⟶ ω) \to (f \circ G^{-1}) : Z ⟶ A$
25	23 24	mpan2	$⊢ f : ω ⟶ A \to (f \circ G^{-1}) : Z ⟶ A$
26	25	3ad2ant1	$⊢ (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to (f \circ G^{-1}) : Z ⟶ A$
27		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
28	1 27	ax-mp	$⊢ M \in ℤ_{\geq M}$
29	28 2	eleqtrri	$⊢ M \in Z$
30		fvco3	$⊢ (G^{-1} : Z ⟶ ω \land M \in Z) \to (f \circ G^{-1}) (M) = f (G^{-1} (M))$
31	23 29 30	mp2an	$⊢ (f \circ G^{-1}) (M) = f (G^{-1} (M))$
32	1 4	om2uz0i	$⊢ G (\emptyset) = M$
33		peano1	$⊢ \emptyset \in ω$
34		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land \emptyset \in ω) \to (G (\emptyset) = M \to G^{-1} (M) = \emptyset)$
35	9 33 34	mp2an	$⊢ G (\emptyset) = M \to G^{-1} (M) = \emptyset$
36	32 35	ax-mp	$⊢ G^{-1} (M) = \emptyset$
37	36	fveq2i	$⊢ f (G^{-1} (M)) = f (\emptyset)$
38	31 37	eqtri	$⊢ (f \circ G^{-1}) (M) = f (\emptyset)$
39		simp2	$⊢ (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to f (\emptyset) = C$
40	38 39	syl5eq	$⊢ (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to (f \circ G^{-1}) (M) = C$
41	23	ffvelrni	$⊢ k \in Z \to G^{-1} (k) \in ω$
42	41	adantl	$⊢ (f : ω ⟶ A \land k \in Z) \to G^{-1} (k) \in ω$
43		suceq	$⊢ m = G^{-1} (k) \to suc m = suc G^{-1} (k)$
44	43	fveq2d	$⊢ m = G^{-1} (k) \to f (suc m) = f (suc G^{-1} (k))$
45		id	$⊢ m = G^{-1} (k) \to m = G^{-1} (k)$
46		fveq2	$⊢ m = G^{-1} (k) \to f (m) = f (G^{-1} (k))$
47	45 46	oveq12d	$⊢ m = G^{-1} (k) \to m H f (m) = G^{-1} (k) H f (G^{-1} (k))$
48	44 47	eleq12d	$⊢ m = G^{-1} (k) \to (f (suc m) \in (m H f (m)) \leftrightarrow f (suc G^{-1} (k)) \in (G^{-1} (k) H f (G^{-1} (k))))$
49	48	rspcv	$⊢ G^{-1} (k) \in ω \to (\forall m \in ω f (suc m) \in (m H f (m)) \to f (suc G^{-1} (k)) \in (G^{-1} (k) H f (G^{-1} (k))))$
50	42 49	syl	$⊢ (f : ω ⟶ A \land k \in Z) \to (\forall m \in ω f (suc m) \in (m H f (m)) \to f (suc G^{-1} (k)) \in (G^{-1} (k) H f (G^{-1} (k))))$
51	2	peano2uzs	$⊢ k \in Z \to k + 1 \in Z$
52		fvco3	$⊢ (G^{-1} : Z ⟶ ω \land k + 1 \in Z) \to (f \circ G^{-1}) (k + 1) = f (G^{-1} (k + 1))$
53	23 51 52	sylancr	$⊢ k \in Z \to (f \circ G^{-1}) (k + 1) = f (G^{-1} (k + 1))$
54	1 4	om2uzsuci	$⊢ G^{-1} (k) \in ω \to G (suc G^{-1} (k)) = G (G^{-1} (k)) + 1$
55	41 54	syl	$⊢ k \in Z \to G (suc G^{-1} (k)) = G (G^{-1} (k)) + 1$
56		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land k \in Z) \to G (G^{-1} (k)) = k$
57	9 56	mpan	$⊢ k \in Z \to G (G^{-1} (k)) = k$
58	57	oveq1d	$⊢ k \in Z \to G (G^{-1} (k)) + 1 = k + 1$
59	55 58	eqtrd	$⊢ k \in Z \to G (suc G^{-1} (k)) = k + 1$
60		peano2	$⊢ G^{-1} (k) \in ω \to suc G^{-1} (k) \in ω$
61	41 60	syl	$⊢ k \in Z \to suc G^{-1} (k) \in ω$
62		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land suc G^{-1} (k) \in ω) \to (G (suc G^{-1} (k)) = k + 1 \to G^{-1} (k + 1) = suc G^{-1} (k))$
63	9 61 62	sylancr	$⊢ k \in Z \to (G (suc G^{-1} (k)) = k + 1 \to G^{-1} (k + 1) = suc G^{-1} (k))$
64	59 63	mpd	$⊢ k \in Z \to G^{-1} (k + 1) = suc G^{-1} (k)$
65	64	fveq2d	$⊢ k \in Z \to f (G^{-1} (k + 1)) = f (suc G^{-1} (k))$
66	53 65	eqtr2d	$⊢ k \in Z \to f (suc G^{-1} (k)) = (f \circ G^{-1}) (k + 1)$
67	66	adantl	$⊢ (f : ω ⟶ A \land k \in Z) \to f (suc G^{-1} (k)) = (f \circ G^{-1}) (k + 1)$
68		ffvelrn	$⊢ (f : ω ⟶ A \land G^{-1} (k) \in ω) \to f (G^{-1} (k)) \in A$
69	41 68	sylan2	$⊢ (f : ω ⟶ A \land k \in Z) \to f (G^{-1} (k)) \in A$
70		fveq2	$⊢ n = G^{-1} (k) \to G (n) = G (G^{-1} (k))$
71	70	oveq1d	$⊢ n = G^{-1} (k) \to G (n) F x = G (G^{-1} (k)) F x$
72		oveq2	$⊢ x = f (G^{-1} (k)) \to G (G^{-1} (k)) F x = G (G^{-1} (k)) F f (G^{-1} (k))$
73		ovex	$⊢ G (G^{-1} (k)) F f (G^{-1} (k)) \in V$
74	71 72 5 73	ovmpo	$⊢ (G^{-1} (k) \in ω \land f (G^{-1} (k)) \in A) \to G^{-1} (k) H f (G^{-1} (k)) = G (G^{-1} (k)) F f (G^{-1} (k))$
75	42 69 74	syl2anc	$⊢ (f : ω ⟶ A \land k \in Z) \to G^{-1} (k) H f (G^{-1} (k)) = G (G^{-1} (k)) F f (G^{-1} (k))$
76		fvco3	$⊢ (G^{-1} : Z ⟶ ω \land k \in Z) \to (f \circ G^{-1}) (k) = f (G^{-1} (k))$
77	23 76	mpan	$⊢ k \in Z \to (f \circ G^{-1}) (k) = f (G^{-1} (k))$
78	77	eqcomd	$⊢ k \in Z \to f (G^{-1} (k)) = (f \circ G^{-1}) (k)$
79	57 78	oveq12d	$⊢ k \in Z \to G (G^{-1} (k)) F f (G^{-1} (k)) = k F (f \circ G^{-1}) (k)$
80	79	adantl	$⊢ (f : ω ⟶ A \land k \in Z) \to G (G^{-1} (k)) F f (G^{-1} (k)) = k F (f \circ G^{-1}) (k)$
81	75 80	eqtrd	$⊢ (f : ω ⟶ A \land k \in Z) \to G^{-1} (k) H f (G^{-1} (k)) = k F (f \circ G^{-1}) (k)$
82	67 81	eleq12d	$⊢ (f : ω ⟶ A \land k \in Z) \to (f (suc G^{-1} (k)) \in (G^{-1} (k) H f (G^{-1} (k))) \leftrightarrow (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k)))$
83	50 82	sylibd	$⊢ (f : ω ⟶ A \land k \in Z) \to (\forall m \in ω f (suc m) \in (m H f (m)) \to (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k)))$
84	83	impancom	$⊢ (f : ω ⟶ A \land \forall m \in ω f (suc m) \in (m H f (m))) \to (k \in Z \to (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k)))$
85	84	ralrimiv	$⊢ (f : ω ⟶ A \land \forall m \in ω f (suc m) \in (m H f (m))) \to \forall k \in Z (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k))$
86	85	3adant2	$⊢ (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to \forall k \in Z (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k))$
87		vex	$⊢ f \in V$
88		rdgfun	$⊢ Fun rec ((y \in V ⟼ y + 1), M)$
89		omex	$⊢ ω \in V$
90		resfunexg	$⊢ (Fun rec ((y \in V ⟼ y + 1), M) \land ω \in V) \to {rec ((y \in V ⟼ y + 1), M) ↾}_{ω} \in V$
91	88 89 90	mp2an	$⊢ {rec ((y \in V ⟼ y + 1), M) ↾}_{ω} \in V$
92	4 91	eqeltri	$⊢ G \in V$
93	92	cnvex	$⊢ G^{-1} \in V$
94	87 93	coex	$⊢ f \circ G^{-1} \in V$
95		feq1	$⊢ g = f \circ G^{-1} \to (g : Z ⟶ A \leftrightarrow (f \circ G^{-1}) : Z ⟶ A)$
96		fveq1	$⊢ g = f \circ G^{-1} \to g (M) = (f \circ G^{-1}) (M)$
97	96	eqeq1d	$⊢ g = f \circ G^{-1} \to (g (M) = C \leftrightarrow (f \circ G^{-1}) (M) = C)$
98		fveq1	$⊢ g = f \circ G^{-1} \to g (k + 1) = (f \circ G^{-1}) (k + 1)$
99		fveq1	$⊢ g = f \circ G^{-1} \to g (k) = (f \circ G^{-1}) (k)$
100	99	oveq2d	$⊢ g = f \circ G^{-1} \to k F g (k) = k F (f \circ G^{-1}) (k)$
101	98 100	eleq12d	$⊢ g = f \circ G^{-1} \to (g (k + 1) \in (k F g (k)) \leftrightarrow (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k)))$
102	101	ralbidv	$⊢ g = f \circ G^{-1} \to (\forall k \in Z g (k + 1) \in (k F g (k)) \leftrightarrow \forall k \in Z (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k)))$
103	95 97 102	3anbi123d	$⊢ g = f \circ G^{-1} \to ((g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k))) \leftrightarrow ((f \circ G^{-1}) : Z ⟶ A \land (f \circ G^{-1}) (M) = C \land \forall k \in Z (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k))))$
104	94 103	spcev	$⊢ ((f \circ G^{-1}) : Z ⟶ A \land (f \circ G^{-1}) (M) = C \land \forall k \in Z (f \circ G^{-1}) (k + 1) \in (k F (f \circ G^{-1}) (k))) \to \exists g (g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k)))$
105	26 40 86 104	syl3anc	$⊢ (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to \exists g (g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k)))$
106	105	exlimiv	$⊢ \exists f (f : ω ⟶ A \land f (\emptyset) = C \land \forall m \in ω f (suc m) \in (m H f (m))) \to \exists g (g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k)))$
107	20 106	syl	$⊢ (C \in A \land F : Z \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : Z ⟶ A \land g (M) = C \land \forall k \in Z g (k + 1) \in (k F g (k)))$

Metamath Proof Explorer

Theorem axdc4uzlem

Proof