Theorem cc2lem 7626

Description: Lemma for cc2 7627. (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 2824	. . . . . . . 8 ⊢ 𝑛 ∈ V
3	2	snex 4320	. . . . . . 7 ⊢ {𝑛} ∈ V
4		cc2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ω)
5		funfvex 5710	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) → (𝐹‘𝑛) ∈ V)
6	5	funfni 5481	. . . . . . . 8 ⊢ ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
7	4, 6	sylan 283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
8		xpexg 4887	. . . . . . 7 ⊢ (({𝑛} ∈ V ∧ (𝐹‘𝑛) ∈ V) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
9	3, 7, 8	sylancr 418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
10		cc2lem.a	. . . . . 6 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
11	9, 10	fmptd 5856	. . . . 5 ⊢ (𝜑 → 𝐴:ω⟶V)
12		sneq 3719	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
13		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
14	12, 13	xpeq12d 4797	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
15		simprr 537	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16		vex 2824	. . . . . . . . . . 11 ⊢ 𝑘 ∈ V
17	16	snex 4320	. . . . . . . . . 10 ⊢ {𝑘} ∈ V
18	4	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19		funfvex 5710	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ V)
20	19	funfni 5481	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹‘𝑘) ∈ V)
21	18, 15, 20	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹‘𝑘) ∈ V)
22		xpexg 4887	. . . . . . . . . 10 ⊢ (({𝑘} ∈ V ∧ (𝐹‘𝑘) ∈ V) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
23	17, 21, 22	sylancr 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
24	10, 14, 15, 23	fvmptd3 5796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑘) = ({𝑘} × (𝐹‘𝑘)))
25	24	eqeq2d 2250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘))))
26		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
27	10	fvmpt2 5786	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
28	26, 9, 27	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
29	28	adantrr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
30	29	eqeq1d 2247	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘))))
31	2	snm 3831	. . . . . . . . . 10 ⊢ ∃𝑤 𝑤 ∈ {𝑛}
32		fveq2 5693	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛))
33	32	eleq2d 2308	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑤 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑛)))
34	33	exbidv 1878	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)))
35		cc2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
36	35	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
37		simprl 535	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
38	34, 36, 37	rspcdva 2934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
39		xp11m 5224	. . . . . . . . . 10 ⊢ ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
40	31, 38, 39	sylancr 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
41	2	sneqr 3883	. . . . . . . . . 10 ⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘)
42	41	adantr 276	. . . . . . . . 9 ⊢ (({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘)) → 𝑛 = 𝑘)
43	40, 42	biimtrdi 163	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) → 𝑛 = 𝑘))
44	30, 43	sylbid 150	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) → 𝑛 = 𝑘))
45	25, 44	sylbid 150	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
46	45	ralrimivva 2632	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
47		dff13 5968	. . . . 5 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
48	11, 46, 47	sylanbrc 421	. . . 4 ⊢ (𝜑 → 𝐴:ω–1-1→V)
49		f1f1orn 5648	. . . . 5 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50		omex 4738	. . . . . 6 ⊢ ω ∈ V
51	50	f1oen 7039	. . . . 5 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52		ensym 7062	. . . . 5 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
53	49, 51, 52	3syl 17	. . . 4 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
54	48, 53	syl 14	. . 3 ⊢ (𝜑 → ran 𝐴 ≈ ω)
55	9	ralrimiva 2623	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V)
56	10	fnmpt 5508	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V → 𝐴 Fn ω)
57	55, 56	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn ω)
58	57	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59		fnfun 5476	. . . . . . 7 ⊢ (𝐴 Fn ω → Fun 𝐴)
60	58, 59	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → Fun 𝐴)
61		simpr 110	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62		elrnrexdm 5841	. . . . . 6 ⊢ (Fun 𝐴 → (𝑧 ∈ ran 𝐴 → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛)))
63	60, 61, 62	sylc 62	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛))
64		simpll 531	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝜑)
65		simprl 535	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ dom 𝐴)
66		fndm 5478	. . . . . . . . 9 ⊢ (𝐴 Fn ω → dom 𝐴 = ω)
67	64, 57, 66	3syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → dom 𝐴 = ω)
68	65, 67	eleqtrd 2317	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ ω)
69	35	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
70	34, 69, 26	rspcdva 2934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
71		eleq1 2301	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ (𝐹‘𝑛) ↔ 𝑎 ∈ (𝐹‘𝑛)))
72	71	cbvexv 1974	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ (𝐹‘𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
73	70, 72	sylib 122	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
74		vsnid 3740	. . . . . . . . . . 11 ⊢ 𝑛 ∈ {𝑛}
75		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → 𝑎 ∈ (𝐹‘𝑛))
76		opelxpi 4804	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
77	74, 75, 76	sylancr 418	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
78		eleq1 2301	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹‘𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛))))
79	78	spcegv 2913	. . . . . . . . . 10 ⊢ (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
80	77, 77, 79	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
81	73, 80	exlimddv 1954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
82	28	eleq2d 2308	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑤 ∈ (𝐴‘𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
83	82	exbidv 1878	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴‘𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
84	81, 83	mpbird 167	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
85	64, 68, 84	syl2anc 415	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
86		simprr 537	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑧 = (𝐴‘𝑛))
87	86	eleq2d 2308	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐴‘𝑛)))
88	87	exbidv 1878	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (∃𝑤 𝑤 ∈ 𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴‘𝑛)))
89	85, 88	mpbird 167	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ 𝑧)
90	63, 89	rexlimddv 2673	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤 ∈ 𝑧)
91	90	ralrimiva 2623	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐴∃𝑤 𝑤 ∈ 𝑧)
92	1, 54, 91	ccfunen 7624	. 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧))
93		vex 2824	. . . . . . . 8 ⊢ 𝑓 ∈ V
94		funfvex 5710	. . . . . . . . . 10 ⊢ ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) → (𝐴‘𝑛) ∈ V)
95	94	funfni 5481	. . . . . . . . 9 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
96	57, 95	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
97		fvexg 5712	. . . . . . . 8 ⊢ ((𝑓 ∈ V ∧ (𝐴‘𝑛) ∈ V) → (𝑓‘(𝐴‘𝑛)) ∈ V)
98	93, 96, 97	sylancr 418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ V)
99		2ndexg 6396	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
100	98, 99	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
101	100	ralrimiva 2623	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
102		cc2lem.g	. . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))
103	102	fnmpt 5508	. . . . 5 ⊢ (∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V → 𝐺 Fn ω)
104	101, 103	syl 14	. . . 4 ⊢ (𝜑 → 𝐺 Fn ω)
105	104	adantr 276	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → 𝐺 Fn ω)
106		simpr 110	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
107		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
108		id 19	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
109	107, 108	eleq12d 2309	. . . . . . . . 9 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
110		simplrr 542	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)
111		fnfvelrn 5834	. . . . . . . . . . 11 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
112	57, 111	sylan 283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
113	112	adantlr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
114	109, 110, 113	rspcdva 2934	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
115	28	eleq2d 2308	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
116	115	adantlr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
117	114, 116	mpbid 147	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)))
118		xp2nd 6394	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
119	117, 118	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
120	102	fvmpt2 5786	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛)) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
121	106, 119, 120	syl2anc 415	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
122	121, 119	eqeltrd 2315	. . . 4 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
123	122	ralrimiva 2623	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))
124	50	a1i 9	. . . . . 6 ⊢ (𝜑 → ω ∈ V)
125		fnex 5931	. . . . . 6 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126	104, 124, 125	syl2anc 415	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
127		fneq1 5467	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128		fveq1 5692	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
129	128	eleq1d 2307	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
130	129	ralbidv 2550	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
131	127, 130	anbi12d 477	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
132	131	spcegv 2913	. . . . 5 ⊢ (𝐺 ∈ V → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
133	126, 132	syl 14	. . . 4 ⊢ (𝜑 → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
134	133	adantr 276	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛))))
135	105, 123, 134	mp2and 437	. 2 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
136	92, 135	exlimddv 1954	1 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209  ∀wral 2528  ∃wrex 2529  Vcvv 2821  {csn 3708  ⟨cop 3711   class class class wbr 4128   ↦ cmpt 4190  ωcom 4735   × cxp 4770  dom cdm 4772  ran crn 4773  Fun wfun 5369   Fn wfn 5370  ⟶wf 5371  –1-1→wf1 5372  –1-1-onto→wf1o 5374  ‘cfv 5375  2^nd c2nd 6367   ≈ cen 7014  CCHOICEwacc 7622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-13 2211  ax-14 2212  ax-ext 2220  ax-coll 4244  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-iinf 4733

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-iun 4012  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-iom 4736  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-2nd 6369  df-er 6801  df-en 7017  df-cc 7623

This theorem is referenced by:  cc2  7627