Theorem cc2lem 7098

Description: Lemma for cc2 7099. (Contributed by Jim Kingdon, 27-Apr-2024.)

Hypotheses

Ref	Expression
cc2.cc	⊢ (𝜑 → CCHOICE)
cc2.a	⊢ (𝜑 → 𝐹 Fn ω)
cc2.m	⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
cc2lem.a	⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
cc2lem.g	⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))

Assertion

Ref	Expression
cc2lem	⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Distinct variable groups:   𝐴,𝑓,𝑛   𝑤,𝐴,𝑛   𝑛,𝐹,𝑤   𝑓,𝐹,𝑔,𝑛   𝑥,𝐹,𝑛,𝑤   𝑔,𝐺,𝑛   𝜑,𝑛,𝑤   𝜑,𝑓

Allowed substitution hints:   𝜑(𝑥,𝑔)   𝐴(𝑥,𝑔)   𝐺(𝑥,𝑤,𝑓)

Proof of Theorem cc2lem

Dummy variables 𝑧 𝑘 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cc2.cc	. . 3 ⊢ (𝜑 → CCHOICE)
2		vex 2692	. . . . . . . 8 ⊢ 𝑛 ∈ V
3	2	snex 4117	. . . . . . 7 ⊢ {𝑛} ∈ V
4		cc2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ω)
5		funfvex 5446	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) → (𝐹‘𝑛) ∈ V)
6	5	funfni 5231	. . . . . . . 8 ⊢ ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
7	4, 6	sylan 281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
8		xpexg 4661	. . . . . . 7 ⊢ (({𝑛} ∈ V ∧ (𝐹‘𝑛) ∈ V) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
9	3, 7, 8	sylancr 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
10		cc2lem.a	. . . . . 6 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
11	9, 10	fmptd 5582	. . . . 5 ⊢ (𝜑 → 𝐴:ω⟶V)
12		sneq 3543	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
13		fveq2 5429	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
14	12, 13	xpeq12d 4572	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
15		simprr 522	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16		vex 2692	. . . . . . . . . . 11 ⊢ 𝑘 ∈ V
17	16	snex 4117	. . . . . . . . . 10 ⊢ {𝑘} ∈ V
18	4	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19		funfvex 5446	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ V)
20	19	funfni 5231	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹‘𝑘) ∈ V)
21	18, 15, 20	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹‘𝑘) ∈ V)
22		xpexg 4661	. . . . . . . . . 10 ⊢ (({𝑘} ∈ V ∧ (𝐹‘𝑘) ∈ V) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
23	17, 21, 22	sylancr 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
24	10, 14, 15, 23	fvmptd3 5522	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑘) = ({𝑘} × (𝐹‘𝑘)))
25	24	eqeq2d 2152	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘))))
26		simpr 109	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
27	10	fvmpt2 5512	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
28	26, 9, 27	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
29	28	adantrr 471	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
30	29	eqeq1d 2149	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘))))
31	2	snm 3651	. . . . . . . . . 10 ⊢ ∃𝑤 𝑤 ∈ {𝑛}
32		fveq2 5429	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛))
33	32	eleq2d 2210	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑤 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑛)))
34	33	exbidv 1798	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)))
35		cc2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
36	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
37		simprl 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
38	34, 36, 37	rspcdva 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
39		xp11m 4985	. . . . . . . . . 10 ⊢ ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
40	31, 38, 39	sylancr 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
41	2	sneqr 3695	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
42	41	adantr 274	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘)) → 𝑛 = 𝑘)
43	40, 42	syl6bi 162	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) → 𝑛 = 𝑘))
44	30, 43	sylbid 149	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) → 𝑛 = 𝑘))
45	25, 44	sylbid 149	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
46	45	ralrimivva 2517	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
47		dff13 5677	. . . . 5 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
48	11, 46, 47	sylanbrc 414	. . . 4 ⊢ (𝜑 → 𝐴:ω–1-1→V)
49		f1f1orn 5386	. . . . 5 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50		omex 4515	. . . . . 6 ⊢ ω ∈ V
51	50	f1oen 6661	. . . . 5 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52		ensym 6683	. . . . 5 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
53	49, 51, 52	3syl 17	. . . 4 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
54	48, 53	syl 14	. . 3 ⊢ (𝜑 → ran 𝐴 ≈ ω)
55	9	ralrimiva 2508	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V)
56	10	fnmpt 5257	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V → 𝐴 Fn ω)
57	55, 56	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn ω)
58	57	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59		fnfun 5228	. . . . . . 7 ⊢ (𝐴 Fn ω → Fun 𝐴)
60	58, 59	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → Fun 𝐴)
61		simpr 109	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62		elrnrexdm 5567	. . . . . 6 ⊢ (Fun 𝐴 → (𝑧 ∈ ran 𝐴 → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛)))
63	60, 61, 62	sylc 62	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛))
64		simpll 519	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝜑)
65		simprl 521	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ dom 𝐴)
66		fndm 5230	. . . . . . . . 9 ⊢ (𝐴 Fn ω → dom 𝐴 = ω)
67	64, 57, 66	3syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → dom 𝐴 = ω)
68	65, 67	eleqtrd 2219	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ ω)
69	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
70	34, 69, 26	rspcdva 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
71		eleq1 2203	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ (𝐹‘𝑛) ↔ 𝑎 ∈ (𝐹‘𝑛)))
72	71	cbvexv 1891	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ (𝐹‘𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
73	70, 72	sylib 121	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
74		vsnid 3564	. . . . . . . . . . 11 ⊢ 𝑛 ∈ {𝑛}
75		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → 𝑎 ∈ (𝐹‘𝑛))
76		opelxpi 4579	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
77	74, 75, 76	sylancr 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
78		eleq1 2203	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹‘𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛))))
79	78	spcegv 2777	. . . . . . . . . 10 ⊢ (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
80	77, 77, 79	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
81	73, 80	exlimddv 1871	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
82	28	eleq2d 2210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑤 ∈ (𝐴‘𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
83	82	exbidv 1798	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴‘𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
84	81, 83	mpbird 166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
85	64, 68, 84	syl2anc 409	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
86		simprr 522	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑧 = (𝐴‘𝑛))
87	86	eleq2d 2210	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐴‘𝑛)))
88	87	exbidv 1798	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (∃𝑤 𝑤 ∈ 𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴‘𝑛)))
89	85, 88	mpbird 166	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ 𝑧)
90	63, 89	rexlimddv 2557	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤 ∈ 𝑧)
91	90	ralrimiva 2508	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐴∃𝑤 𝑤 ∈ 𝑧)
92	1, 54, 91	ccfunen 7096	. 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧))
93		vex 2692	. . . . . . . 8 ⊢ 𝑓 ∈ V
94		funfvex 5446	. . . . . . . . . 10 ⊢ ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) → (𝐴‘𝑛) ∈ V)
95	94	funfni 5231	. . . . . . . . 9 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
96	57, 95	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
97		fvexg 5448	. . . . . . . 8 ⊢ ((𝑓 ∈ V ∧ (𝐴‘𝑛) ∈ V) → (𝑓‘(𝐴‘𝑛)) ∈ V)
98	93, 96, 97	sylancr 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ V)
99		2ndexg 6074	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
100	98, 99	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
101	100	ralrimiva 2508	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
102		cc2lem.g	. . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))
103	102	fnmpt 5257	. . . . 5 ⊢ (∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V → 𝐺 Fn ω)
104	101, 103	syl 14	. . . 4 ⊢ (𝜑 → 𝐺 Fn ω)
105	104	adantr 274	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → 𝐺 Fn ω)
106		simpr 109	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
107		fveq2 5429	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
108		id 19	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
109	107, 108	eleq12d 2211	. . . . . . . . 9 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
110		simplrr 526	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)
111		fnfvelrn 5560	. . . . . . . . . . 11 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
112	57, 111	sylan 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
113	112	adantlr 469	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
114	109, 110, 113	rspcdva 2798	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
115	28	eleq2d 2210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
116	115	adantlr 469	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
117	114, 116	mpbid 146	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)))
118		xp2nd 6072	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
119	117, 118	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
120	102	fvmpt2 5512	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛)) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
121	106, 119, 120	syl2anc 409	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
122	121, 119	eqeltrd 2217	. . . 4 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
123	122	ralrimiva 2508	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))
124	50	a1i 9	. . . . . 6 ⊢ (𝜑 → ω ∈ V)
125		fnex 5650	. . . . . 6 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126	104, 124, 125	syl2anc 409	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
127		fneq1 5219	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128		fveq1 5428	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
129	128	eleq1d 2209	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
130	129	ralbidv 2438	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
131	127, 130	anbi12d 465	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
132	131	spcegv 2777	. . . . 5 ⊢ (𝐺 ∈ V → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
133	126, 132	syl 14	. . . 4 ⊢ (𝜑 → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
134	133	adantr 274	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
135	105, 123, 134	mp2and 430	. 2 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
136	92, 135	exlimddv 1871	1 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689  {csn 3532  ⟨cop 3535   class class class wbr 3937   ↦ cmpt 3997  ωcom 4512   × cxp 4545  dom cdm 4547  ran crn 4548  Fun wfun 5125   Fn wfn 5126  ⟶wf 5127  –1-1→wf1 5128  –1-1-onto→wf1o 5130  ‘cfv 5131  2^nd c2nd 6045   ≈ cen 6640  CCHOICEwacc 7094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-iinf 4510

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-2nd 6047  df-er 6437  df-en 6643  df-cc 7095

This theorem is referenced by:  cc2  7099