axdc4lem

	Ref	Expression
Hypotheses	axdc4lem.1	$⊢ A \in V$
	axdc4lem.2	$⊢ G = (n \in ω, x \in A ⟼ \{suc n\} \times (n F x))$
Assertion	axdc4lem	$⊢ (C \in A \land F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k)))$

Proof

Step	Hyp	Ref	Expression
1		axdc4lem.1	$⊢ A \in V$
2		axdc4lem.2	$⊢ G = (n \in ω, x \in A ⟼ \{suc n\} \times (n F x))$
3		peano1	$⊢ \emptyset \in ω$
4		opelxpi	$⊢ (\emptyset \in ω \land C \in A) \to ⟨\emptyset, C⟩ \in (ω \times A)$
5	3 4	mpan	$⊢ C \in A \to ⟨\emptyset, C⟩ \in (ω \times A)$
6		simp2	$⊢ (F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to n \in ω$
7		fovrn	$⊢ (F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to n F x \in (𝒫 A ∖ \{\emptyset\})$
8		peano2	$⊢ n \in ω \to suc n \in ω$
9	8	snssd	$⊢ n \in ω \to \{suc n\} \subseteq ω$
10		eldifi	$⊢ n F x \in (𝒫 A ∖ \{\emptyset\}) \to n F x \in 𝒫 A$
11	1	elpw2	$⊢ n F x \in 𝒫 A \leftrightarrow n F x \subseteq A$
12		xpss12	$⊢ (\{suc n\} \subseteq ω \land n F x \subseteq A) \to \{suc n\} \times (n F x) \subseteq ω \times A$
13	11 12	sylan2b	$⊢ (\{suc n\} \subseteq ω \land n F x \in 𝒫 A) \to \{suc n\} \times (n F x) \subseteq ω \times A$
14	9 10 13	syl2an	$⊢ (n \in ω \land n F x \in (𝒫 A ∖ \{\emptyset\})) \to \{suc n\} \times (n F x) \subseteq ω \times A$
15		snex	$⊢ \{suc n\} \in V$
16		ovex	$⊢ n F x \in V$
17	15 16	xpex	$⊢ \{suc n\} \times (n F x) \in V$
18	17	elpw	$⊢ \{suc n\} \times (n F x) \in 𝒫 (ω \times A) \leftrightarrow \{suc n\} \times (n F x) \subseteq ω \times A$
19	14 18	sylibr	$⊢ (n \in ω \land n F x \in (𝒫 A ∖ \{\emptyset\})) \to \{suc n\} \times (n F x) \in 𝒫 (ω \times A)$
20	6 7 19	syl2anc	$⊢ (F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to \{suc n\} \times (n F x) \in 𝒫 (ω \times A)$
21		eldifn	$⊢ n F x \in (𝒫 A ∖ \{\emptyset\}) \to \neg n F x \in \{\emptyset\}$
22	16	elsn	$⊢ n F x \in \{\emptyset\} \leftrightarrow n F x = \emptyset$
23	22	necon3bbii	$⊢ \neg n F x \in \{\emptyset\} \leftrightarrow n F x \neq \emptyset$
24		vex	$⊢ n \in V$
25	24	sucex	$⊢ suc n \in V$
26	25	snnz	$⊢ \{suc n\} \neq \emptyset$
27		xpnz	$⊢ (\{suc n\} \neq \emptyset \land n F x \neq \emptyset) \leftrightarrow \{suc n\} \times (n F x) \neq \emptyset$
28	27	biimpi	$⊢ (\{suc n\} \neq \emptyset \land n F x \neq \emptyset) \to \{suc n\} \times (n F x) \neq \emptyset$
29	26 28	mpan	$⊢ n F x \neq \emptyset \to \{suc n\} \times (n F x) \neq \emptyset$
30	23 29	sylbi	$⊢ \neg n F x \in \{\emptyset\} \to \{suc n\} \times (n F x) \neq \emptyset$
31	17	elsn	$⊢ \{suc n\} \times (n F x) \in \{\emptyset\} \leftrightarrow \{suc n\} \times (n F x) = \emptyset$
32	31	necon3bbii	$⊢ \neg \{suc n\} \times (n F x) \in \{\emptyset\} \leftrightarrow \{suc n\} \times (n F x) \neq \emptyset$
33	30 32	sylibr	$⊢ \neg n F x \in \{\emptyset\} \to \neg \{suc n\} \times (n F x) \in \{\emptyset\}$
34	7 21 33	3syl	$⊢ (F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to \neg \{suc n\} \times (n F x) \in \{\emptyset\}$
35	20 34	eldifd	$⊢ (F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \land n \in ω \land x \in A) \to \{suc n\} \times (n F x) \in (𝒫 (ω \times A) ∖ \{\emptyset\})$
36	35	3expib	$⊢ F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \to ((n \in ω \land x \in A) \to \{suc n\} \times (n F x) \in (𝒫 (ω \times A) ∖ \{\emptyset\}))$
37	36	ralrimivv	$⊢ F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \to \forall n \in ω \forall x \in A \{suc n\} \times (n F x) \in (𝒫 (ω \times A) ∖ \{\emptyset\})$
38	2	fmpo	$⊢ \forall n \in ω \forall x \in A \{suc n\} \times (n F x) \in (𝒫 (ω \times A) ∖ \{\emptyset\}) \leftrightarrow G : ω \times A ⟶ 𝒫 (ω \times A) ∖ \{\emptyset\}$
39	37 38	sylib	$⊢ F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\} \to G : ω \times A ⟶ 𝒫 (ω \times A) ∖ \{\emptyset\}$
40		dcomex	$⊢ ω \in V$
41	40 1	xpex	$⊢ ω \times A \in V$
42	41	axdc3	$⊢ (⟨\emptyset, C⟩ \in (ω \times A) \land G : ω \times A ⟶ 𝒫 (ω \times A) ∖ \{\emptyset\}) \to \exists h (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))$
43	5 39 42	syl2an	$⊢ (C \in A \land F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists h (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))$
44		2ndcof	$⊢ h : ω ⟶ ω \times A \to (2^{nd} \circ h) : ω ⟶ A$
45	44	3ad2ant1	$⊢ (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to (2^{nd} \circ h) : ω ⟶ A$
46	45	adantl	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (2^{nd} \circ h) : ω ⟶ A$
47		fex2	$⊢ ((2^{nd} \circ h) : ω ⟶ A \land ω \in V \land A \in V) \to 2^{nd} \circ h \in V$
48	40 1 47	mp3an23	$⊢ (2^{nd} \circ h) : ω ⟶ A \to 2^{nd} \circ h \in V$
49	46 48	syl	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to 2^{nd} \circ h \in V$
50		fvco3	$⊢ (h : ω ⟶ ω \times A \land \emptyset \in ω) \to (2^{nd} \circ h) (\emptyset) = 2^{nd} (h (\emptyset))$
51	3 50	mpan2	$⊢ h : ω ⟶ ω \times A \to (2^{nd} \circ h) (\emptyset) = 2^{nd} (h (\emptyset))$
52	51	3ad2ant1	$⊢ (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to (2^{nd} \circ h) (\emptyset) = 2^{nd} (h (\emptyset))$
53		fveq2	$⊢ h (\emptyset) = ⟨\emptyset, C⟩ \to 2^{nd} (h (\emptyset)) = 2^{nd} (⟨\emptyset, C⟩)$
54	53	3ad2ant2	$⊢ (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to 2^{nd} (h (\emptyset)) = 2^{nd} (⟨\emptyset, C⟩)$
55	52 54	eqtrd	$⊢ (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to (2^{nd} \circ h) (\emptyset) = 2^{nd} (⟨\emptyset, C⟩)$
56		op2ndg	$⊢ (\emptyset \in ω \land C \in A) \to 2^{nd} (⟨\emptyset, C⟩) = C$
57	3 56	mpan	$⊢ C \in A \to 2^{nd} (⟨\emptyset, C⟩) = C$
58	55 57	sylan9eqr	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (2^{nd} \circ h) (\emptyset) = C$
59		nfv	$⊢ Ⅎ k C \in A$
60		nfv	$⊢ Ⅎ k h : ω ⟶ ω \times A$
61		nfv	$⊢ Ⅎ k h (\emptyset) = ⟨\emptyset, C⟩$
62		nfra1	$⊢ Ⅎ k \forall k \in ω h (suc k) \in G (h (k))$
63	60 61 62	nf3an	$⊢ Ⅎ k (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))$
64	59 63	nfan	$⊢ Ⅎ k (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))))$
65		fveq2	$⊢ m = \emptyset \to h (m) = h (\emptyset)$
66		opeq1	$⊢ m = \emptyset \to ⟨m, z⟩ = ⟨\emptyset, z⟩$
67	65 66	eqeq12d	$⊢ m = \emptyset \to (h (m) = ⟨m, z⟩ \leftrightarrow h (\emptyset) = ⟨\emptyset, z⟩)$
68	67	exbidv	$⊢ m = \emptyset \to (\exists z h (m) = ⟨m, z⟩ \leftrightarrow \exists z h (\emptyset) = ⟨\emptyset, z⟩)$
69		fveq2	$⊢ m = i \to h (m) = h (i)$
70		opeq1	$⊢ m = i \to ⟨m, z⟩ = ⟨i, z⟩$
71	69 70	eqeq12d	$⊢ m = i \to (h (m) = ⟨m, z⟩ \leftrightarrow h (i) = ⟨i, z⟩)$
72	71	exbidv	$⊢ m = i \to (\exists z h (m) = ⟨m, z⟩ \leftrightarrow \exists z h (i) = ⟨i, z⟩)$
73		fveq2	$⊢ m = suc i \to h (m) = h (suc i)$
74		opeq1	$⊢ m = suc i \to ⟨m, z⟩ = ⟨suc i, z⟩$
75	73 74	eqeq12d	$⊢ m = suc i \to (h (m) = ⟨m, z⟩ \leftrightarrow h (suc i) = ⟨suc i, z⟩)$
76	75	exbidv	$⊢ m = suc i \to (\exists z h (m) = ⟨m, z⟩ \leftrightarrow \exists z h (suc i) = ⟨suc i, z⟩)$
77		opeq2	$⊢ z = C \to ⟨\emptyset, z⟩ = ⟨\emptyset, C⟩$
78	77	eqeq2d	$⊢ z = C \to (h (\emptyset) = ⟨\emptyset, z⟩ \leftrightarrow h (\emptyset) = ⟨\emptyset, C⟩)$
79	78	spcegv	$⊢ C \in A \to (h (\emptyset) = ⟨\emptyset, C⟩ \to \exists z h (\emptyset) = ⟨\emptyset, z⟩)$
80	79	imp	$⊢ (C \in A \land h (\emptyset) = ⟨\emptyset, C⟩) \to \exists z h (\emptyset) = ⟨\emptyset, z⟩$
81	80	3ad2antr2	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to \exists z h (\emptyset) = ⟨\emptyset, z⟩$
82		fveq2	$⊢ h (i) = ⟨i, z⟩ \to G (h (i)) = G (⟨i, z⟩)$
83		df-ov	$⊢ i G z = G (⟨i, z⟩)$
84	82 83	eqtr4di	$⊢ h (i) = ⟨i, z⟩ \to G (h (i)) = i G z$
85	84	adantl	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to G (h (i)) = i G z$
86		simplr	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to i \in ω$
87		ffvelrn	$⊢ (h : ω ⟶ ω \times A \land i \in ω) \to h (i) \in (ω \times A)$
88		eleq1	$⊢ h (i) = ⟨i, z⟩ \to (h (i) \in (ω \times A) \leftrightarrow ⟨i, z⟩ \in (ω \times A))$
89		opelxp2	$⊢ ⟨i, z⟩ \in (ω \times A) \to z \in A$
90	88 89	syl6bi	$⊢ h (i) = ⟨i, z⟩ \to (h (i) \in (ω \times A) \to z \in A)$
91	87 90	mpan9	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to z \in A$
92		suceq	$⊢ n = i \to suc n = suc i$
93	92	sneqd	$⊢ n = i \to \{suc n\} = \{suc i\}$
94		oveq1	$⊢ n = i \to n F x = i F x$
95	93 94	xpeq12d	$⊢ n = i \to \{suc n\} \times (n F x) = \{suc i\} \times (i F x)$
96		oveq2	$⊢ x = z \to i F x = i F z$
97	96	xpeq2d	$⊢ x = z \to \{suc i\} \times (i F x) = \{suc i\} \times (i F z)$
98		snex	$⊢ \{suc i\} \in V$
99		ovex	$⊢ i F z \in V$
100	98 99	xpex	$⊢ \{suc i\} \times (i F z) \in V$
101	95 97 2 100	ovmpo	$⊢ (i \in ω \land z \in A) \to i G z = \{suc i\} \times (i F z)$
102	86 91 101	syl2anc	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to i G z = \{suc i\} \times (i F z)$
103	85 102	eqtrd	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to G (h (i)) = \{suc i\} \times (i F z)$
104		suceq	$⊢ k = i \to suc k = suc i$
105	104	fveq2d	$⊢ k = i \to h (suc k) = h (suc i)$
106		2fveq3	$⊢ k = i \to G (h (k)) = G (h (i))$
107	105 106	eleq12d	$⊢ k = i \to (h (suc k) \in G (h (k)) \leftrightarrow h (suc i) \in G (h (i)))$
108	107	rspcv	$⊢ i \in ω \to (\forall k \in ω h (suc k) \in G (h (k)) \to h (suc i) \in G (h (i)))$
109	108	ad2antlr	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to (\forall k \in ω h (suc k) \in G (h (k)) \to h (suc i) \in G (h (i)))$
110		eleq2	$⊢ G (h (i)) = \{suc i\} \times (i F z) \to (h (suc i) \in G (h (i)) \leftrightarrow h (suc i) \in (\{suc i\} \times (i F z)))$
111		elxp	$⊢ h (suc i) \in (\{suc i\} \times (i F z)) \leftrightarrow \exists s \exists t (h (suc i) = ⟨s, t⟩ \land (s \in \{suc i\} \land t \in (i F z)))$
112		velsn	$⊢ s \in \{suc i\} \leftrightarrow s = suc i$
113		opeq1	$⊢ s = suc i \to ⟨s, t⟩ = ⟨suc i, t⟩$
114	112 113	sylbi	$⊢ s \in \{suc i\} \to ⟨s, t⟩ = ⟨suc i, t⟩$
115	114	eqeq2d	$⊢ s \in \{suc i\} \to (h (suc i) = ⟨s, t⟩ \leftrightarrow h (suc i) = ⟨suc i, t⟩)$
116	115	biimpac	$⊢ (h (suc i) = ⟨s, t⟩ \land s \in \{suc i\}) \to h (suc i) = ⟨suc i, t⟩$
117	116	adantrr	$⊢ (h (suc i) = ⟨s, t⟩ \land (s \in \{suc i\} \land t \in (i F z))) \to h (suc i) = ⟨suc i, t⟩$
118	117	eximi	$⊢ \exists t (h (suc i) = ⟨s, t⟩ \land (s \in \{suc i\} \land t \in (i F z))) \to \exists t h (suc i) = ⟨suc i, t⟩$
119	118	exlimiv	$⊢ \exists s \exists t (h (suc i) = ⟨s, t⟩ \land (s \in \{suc i\} \land t \in (i F z))) \to \exists t h (suc i) = ⟨suc i, t⟩$
120	111 119	sylbi	$⊢ h (suc i) \in (\{suc i\} \times (i F z)) \to \exists t h (suc i) = ⟨suc i, t⟩$
121	110 120	syl6bi	$⊢ G (h (i)) = \{suc i\} \times (i F z) \to (h (suc i) \in G (h (i)) \to \exists t h (suc i) = ⟨suc i, t⟩)$
122	103 109 121	sylsyld	$⊢ ((h : ω ⟶ ω \times A \land i \in ω) \land h (i) = ⟨i, z⟩) \to (\forall k \in ω h (suc k) \in G (h (k)) \to \exists t h (suc i) = ⟨suc i, t⟩)$
123	122	expcom	$⊢ h (i) = ⟨i, z⟩ \to ((h : ω ⟶ ω \times A \land i \in ω) \to (\forall k \in ω h (suc k) \in G (h (k)) \to \exists t h (suc i) = ⟨suc i, t⟩))$
124	123	exlimiv	$⊢ \exists z h (i) = ⟨i, z⟩ \to ((h : ω ⟶ ω \times A \land i \in ω) \to (\forall k \in ω h (suc k) \in G (h (k)) \to \exists t h (suc i) = ⟨suc i, t⟩))$
125	124	com3l	$⊢ (h : ω ⟶ ω \times A \land i \in ω) \to (\forall k \in ω h (suc k) \in G (h (k)) \to (\exists z h (i) = ⟨i, z⟩ \to \exists t h (suc i) = ⟨suc i, t⟩))$
126		opeq2	$⊢ t = z \to ⟨suc i, t⟩ = ⟨suc i, z⟩$
127	126	eqeq2d	$⊢ t = z \to (h (suc i) = ⟨suc i, t⟩ \leftrightarrow h (suc i) = ⟨suc i, z⟩)$
128	127	cbvexvw	$⊢ \exists t h (suc i) = ⟨suc i, t⟩ \leftrightarrow \exists z h (suc i) = ⟨suc i, z⟩$
129	125 128	syl8ib	$⊢ (h : ω ⟶ ω \times A \land i \in ω) \to (\forall k \in ω h (suc k) \in G (h (k)) \to (\exists z h (i) = ⟨i, z⟩ \to \exists z h (suc i) = ⟨suc i, z⟩))$
130	129	impancom	$⊢ (h : ω ⟶ ω \times A \land \forall k \in ω h (suc k) \in G (h (k))) \to (i \in ω \to (\exists z h (i) = ⟨i, z⟩ \to \exists z h (suc i) = ⟨suc i, z⟩))$
131	130	3adant2	$⊢ (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to (i \in ω \to (\exists z h (i) = ⟨i, z⟩ \to \exists z h (suc i) = ⟨suc i, z⟩))$
132	131	adantl	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (i \in ω \to (\exists z h (i) = ⟨i, z⟩ \to \exists z h (suc i) = ⟨suc i, z⟩))$
133	132	com12	$⊢ i \in ω \to ((C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (\exists z h (i) = ⟨i, z⟩ \to \exists z h (suc i) = ⟨suc i, z⟩))$
134	68 72 76 81 133	finds2	$⊢ m \in ω \to ((C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to \exists z h (m) = ⟨m, z⟩)$
135	134	com12	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (m \in ω \to \exists z h (m) = ⟨m, z⟩)$
136	135	ralrimiv	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to \forall m \in ω \exists z h (m) = ⟨m, z⟩$
137		fveq2	$⊢ m = k \to h (m) = h (k)$
138		opeq1	$⊢ m = k \to ⟨m, z⟩ = ⟨k, z⟩$
139	137 138	eqeq12d	$⊢ m = k \to (h (m) = ⟨m, z⟩ \leftrightarrow h (k) = ⟨k, z⟩)$
140	139	exbidv	$⊢ m = k \to (\exists z h (m) = ⟨m, z⟩ \leftrightarrow \exists z h (k) = ⟨k, z⟩)$
141	140	rspccv	$⊢ \forall m \in ω \exists z h (m) = ⟨m, z⟩ \to (k \in ω \to \exists z h (k) = ⟨k, z⟩)$
142	136 141	syl	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (k \in ω \to \exists z h (k) = ⟨k, z⟩)$
143	142	3impia	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to \exists z h (k) = ⟨k, z⟩$
144		simp21	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h : ω ⟶ ω \times A$
145		simp3	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to k \in ω$
146		rspa	$⊢ (\forall k \in ω h (suc k) \in G (h (k)) \land k \in ω) \to h (suc k) \in G (h (k))$
147	146	3ad2antl3	$⊢ ((h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h (suc k) \in G (h (k))$
148	147	3adant1	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h (suc k) \in G (h (k))$
149		simpl	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to h (k) = ⟨k, z⟩$
150	149	fveq2d	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to G (h (k)) = G (⟨k, z⟩)$
151		simprr	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to k \in ω$
152		eleq1	$⊢ h (k) = ⟨k, z⟩ \to (h (k) \in (ω \times A) \leftrightarrow ⟨k, z⟩ \in (ω \times A))$
153		opelxp2	$⊢ ⟨k, z⟩ \in (ω \times A) \to z \in A$
154	152 153	syl6bi	$⊢ h (k) = ⟨k, z⟩ \to (h (k) \in (ω \times A) \to z \in A)$
155		ffvelrn	$⊢ (h : ω ⟶ ω \times A \land k \in ω) \to h (k) \in (ω \times A)$
156	154 155	impel	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to z \in A$
157		df-ov	$⊢ k G z = G (⟨k, z⟩)$
158		suceq	$⊢ n = k \to suc n = suc k$
159	158	sneqd	$⊢ n = k \to \{suc n\} = \{suc k\}$
160		oveq1	$⊢ n = k \to n F x = k F x$
161	159 160	xpeq12d	$⊢ n = k \to \{suc n\} \times (n F x) = \{suc k\} \times (k F x)$
162		oveq2	$⊢ x = z \to k F x = k F z$
163	162	xpeq2d	$⊢ x = z \to \{suc k\} \times (k F x) = \{suc k\} \times (k F z)$
164		snex	$⊢ \{suc k\} \in V$
165		ovex	$⊢ k F z \in V$
166	164 165	xpex	$⊢ \{suc k\} \times (k F z) \in V$
167	161 163 2 166	ovmpo	$⊢ (k \in ω \land z \in A) \to k G z = \{suc k\} \times (k F z)$
168	157 167	eqtr3id	$⊢ (k \in ω \land z \in A) \to G (⟨k, z⟩) = \{suc k\} \times (k F z)$
169	151 156 168	syl2anc	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to G (⟨k, z⟩) = \{suc k\} \times (k F z)$
170	150 169	eqtrd	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to G (h (k)) = \{suc k\} \times (k F z)$
171	170	eleq2d	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to (h (suc k) \in G (h (k)) \leftrightarrow h (suc k) \in (\{suc k\} \times (k F z)))$
172		elxp	$⊢ h (suc k) \in (\{suc k\} \times (k F z)) \leftrightarrow \exists s \exists t (h (suc k) = ⟨s, t⟩ \land (s \in \{suc k\} \land t \in (k F z)))$
173		peano2	$⊢ k \in ω \to suc k \in ω$
174		fvco3	$⊢ (h : ω ⟶ ω \times A \land suc k \in ω) \to (2^{nd} \circ h) (suc k) = 2^{nd} (h (suc k))$
175	173 174	sylan2	$⊢ (h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) = 2^{nd} (h (suc k))$
176	175	adantl	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (suc k) = 2^{nd} (h (suc k))$
177		simpll	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to h (suc k) = ⟨s, t⟩$
178	177	fveq2d	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to 2^{nd} (h (suc k)) = 2^{nd} (⟨s, t⟩)$
179	176 178	eqtrd	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (suc k) = 2^{nd} (⟨s, t⟩)$
180		vex	$⊢ s \in V$
181		vex	$⊢ t \in V$
182	180 181	op2nd	$⊢ 2^{nd} (⟨s, t⟩) = t$
183	179 182	eqtrdi	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (suc k) = t$
184		fvco3	$⊢ (h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (k) = 2^{nd} (h (k))$
185	184	adantl	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (k) = 2^{nd} (h (k))$
186		simplr	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to h (k) = ⟨k, z⟩$
187	186	fveq2d	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to 2^{nd} (h (k)) = 2^{nd} (⟨k, z⟩)$
188	185 187	eqtrd	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (k) = 2^{nd} (⟨k, z⟩)$
189		vex	$⊢ k \in V$
190		vex	$⊢ z \in V$
191	189 190	op2nd	$⊢ 2^{nd} (⟨k, z⟩) = z$
192	188 191	eqtrdi	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (k) = z$
193	192	oveq2d	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to k F (2^{nd} \circ h) (k) = k F z$
194	183 193	eleq12d	$⊢ ((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to ((2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)) \leftrightarrow t \in (k F z))$
195	194	biimprcd	$⊢ t \in (k F z) \to (((h (suc k) = ⟨s, t⟩ \land h (k) = ⟨k, z⟩) \land (h : ω ⟶ ω \times A \land k \in ω)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
196	195	exp4c	$⊢ t \in (k F z) \to (h (suc k) = ⟨s, t⟩ \to (h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))))$
197	196	adantl	$⊢ (s \in \{suc k\} \land t \in (k F z)) \to (h (suc k) = ⟨s, t⟩ \to (h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))))$
198	197	impcom	$⊢ (h (suc k) = ⟨s, t⟩ \land (s \in \{suc k\} \land t \in (k F z))) \to (h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
199	198	exlimivv	$⊢ \exists s \exists t (h (suc k) = ⟨s, t⟩ \land (s \in \{suc k\} \land t \in (k F z))) \to (h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
200	172 199	sylbi	$⊢ h (suc k) \in (\{suc k\} \times (k F z)) \to (h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
201	200	com3l	$⊢ h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (h (suc k) \in (\{suc k\} \times (k F z)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
202	201	imp	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to (h (suc k) \in (\{suc k\} \times (k F z)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
203	171 202	sylbid	$⊢ (h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω)) \to (h (suc k) \in G (h (k)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
204	203	ex	$⊢ h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (h (suc k) \in G (h (k)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
205	204	exlimiv	$⊢ \exists z h (k) = ⟨k, z⟩ \to ((h : ω ⟶ ω \times A \land k \in ω) \to (h (suc k) \in G (h (k)) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
206	205	3imp	$⊢ (\exists z h (k) = ⟨k, z⟩ \land (h : ω ⟶ ω \times A \land k \in ω) \land h (suc k) \in G (h (k))) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))$
207	143 144 145 148 206	syl121anc	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))$
208	207	3expia	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to (k \in ω \to (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
209	64 208	ralrimi	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to \forall k \in ω (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))$
210	46 58 209	3jca	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to ((2^{nd} \circ h) : ω ⟶ A \land (2^{nd} \circ h) (\emptyset) = C \land \forall k \in ω (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
211		feq1	$⊢ g = 2^{nd} \circ h \to (g : ω ⟶ A \leftrightarrow (2^{nd} \circ h) : ω ⟶ A)$
212		fveq1	$⊢ g = 2^{nd} \circ h \to g (\emptyset) = (2^{nd} \circ h) (\emptyset)$
213	212	eqeq1d	$⊢ g = 2^{nd} \circ h \to (g (\emptyset) = C \leftrightarrow (2^{nd} \circ h) (\emptyset) = C)$
214		fveq1	$⊢ g = 2^{nd} \circ h \to g (suc k) = (2^{nd} \circ h) (suc k)$
215		fveq1	$⊢ g = 2^{nd} \circ h \to g (k) = (2^{nd} \circ h) (k)$
216	215	oveq2d	$⊢ g = 2^{nd} \circ h \to k F g (k) = k F (2^{nd} \circ h) (k)$
217	214 216	eleq12d	$⊢ g = 2^{nd} \circ h \to (g (suc k) \in (k F g (k)) \leftrightarrow (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
218	217	ralbidv	$⊢ g = 2^{nd} \circ h \to (\forall k \in ω g (suc k) \in (k F g (k)) \leftrightarrow \forall k \in ω (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k)))$
219	211 213 218	3anbi123d	$⊢ g = 2^{nd} \circ h \to ((g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k))) \leftrightarrow ((2^{nd} \circ h) : ω ⟶ A \land (2^{nd} \circ h) (\emptyset) = C \land \forall k \in ω (2^{nd} \circ h) (suc k) \in (k F (2^{nd} \circ h) (k))))$
220	49 210 219	spcedv	$⊢ (C \in A \land (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k)))) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k)))$
221	220	ex	$⊢ C \in A \to ((h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k))))$
222	221	exlimdv	$⊢ C \in A \to (\exists h (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k))))$
223	222	adantr	$⊢ (C \in A \land F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to (\exists h (h : ω ⟶ ω \times A \land h (\emptyset) = ⟨\emptyset, C⟩ \land \forall k \in ω h (suc k) \in G (h (k))) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k))))$
224	43 223	mpd	$⊢ (C \in A \land F : ω \times A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in (k F g (k)))$

Metamath Proof Explorer

Theorem axdc4lem

Proof