Theorem cc2lem 7333

Description: Lemma for cc2 7334. (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 2766	. . . . . . . 8 ⊢ 𝑛 ∈ V
3	2	snex 4218	. . . . . . 7 ⊢ {𝑛} ∈ V
4		cc2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ω)
5		funfvex 5575	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) → (𝐹‘𝑛) ∈ V)
6	5	funfni 5358	. . . . . . . 8 ⊢ ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
7	4, 6	sylan 283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
8		xpexg 4777	. . . . . . 7 ⊢ (({𝑛} ∈ V ∧ (𝐹‘𝑛) ∈ V) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
9	3, 7, 8	sylancr 414	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
10		cc2lem.a	. . . . . 6 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
11	9, 10	fmptd 5716	. . . . 5 ⊢ (𝜑 → 𝐴:ω⟶V)
12		sneq 3633	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
13		fveq2 5558	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
14	12, 13	xpeq12d 4688	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
15		simprr 531	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16		vex 2766	. . . . . . . . . . 11 ⊢ 𝑘 ∈ V
17	16	snex 4218	. . . . . . . . . 10 ⊢ {𝑘} ∈ V
18	4	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19		funfvex 5575	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ V)
20	19	funfni 5358	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹‘𝑘) ∈ V)
21	18, 15, 20	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹‘𝑘) ∈ V)
22		xpexg 4777	. . . . . . . . . 10 ⊢ (({𝑘} ∈ V ∧ (𝐹‘𝑘) ∈ V) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
23	17, 21, 22	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
24	10, 14, 15, 23	fvmptd3 5655	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑘) = ({𝑘} × (𝐹‘𝑘)))
25	24	eqeq2d 2208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘))))
26		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
27	10	fvmpt2 5645	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
28	26, 9, 27	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
29	28	adantrr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
30	29	eqeq1d 2205	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘))))
31	2	snm 3742	. . . . . . . . . 10 ⊢ ∃𝑤 𝑤 ∈ {𝑛}
32		fveq2 5558	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛))
33	32	eleq2d 2266	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑤 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑛)))
34	33	exbidv 1839	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)))
35		cc2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
36	35	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
37		simprl 529	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
38	34, 36, 37	rspcdva 2873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
39		xp11m 5108	. . . . . . . . . 10 ⊢ ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
40	31, 38, 39	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
41	2	sneqr 3790	. . . . . . . . . 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 2579	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
47		dff13 5815	. . . . 5 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
48	11, 46, 47	sylanbrc 417	. . . 4 ⊢ (𝜑 → 𝐴:ω–1-1→V)
49		f1f1orn 5515	. . . . 5 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50		omex 4629	. . . . . 6 ⊢ ω ∈ V
51	50	f1oen 6818	. . . . 5 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52		ensym 6840	. . . . 5 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
53	49, 51, 52	3syl 17	. . . 4 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
54	48, 53	syl 14	. . 3 ⊢ (𝜑 → ran 𝐴 ≈ ω)
55	9	ralrimiva 2570	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V)
56	10	fnmpt 5384	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V → 𝐴 Fn ω)
57	55, 56	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn ω)
58	57	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59		fnfun 5355	. . . . . . 7 ⊢ (𝐴 Fn ω → Fun 𝐴)
60	58, 59	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → Fun 𝐴)
61		simpr 110	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62		elrnrexdm 5701	. . . . . 6 ⊢ (Fun 𝐴 → (𝑧 ∈ ran 𝐴 → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛)))
63	60, 61, 62	sylc 62	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛))
64		simpll 527	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝜑)
65		simprl 529	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ dom 𝐴)
66		fndm 5357	. . . . . . . . 9 ⊢ (𝐴 Fn ω → dom 𝐴 = ω)
67	64, 57, 66	3syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → dom 𝐴 = ω)
68	65, 67	eleqtrd 2275	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ ω)
69	35	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
70	34, 69, 26	rspcdva 2873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
71		eleq1 2259	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ (𝐹‘𝑛) ↔ 𝑎 ∈ (𝐹‘𝑛)))
72	71	cbvexv 1933	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ (𝐹‘𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
73	70, 72	sylib 122	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
74		vsnid 3654	. . . . . . . . . . 11 ⊢ 𝑛 ∈ {𝑛}
75		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → 𝑎 ∈ (𝐹‘𝑛))
76		opelxpi 4695	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
77	74, 75, 76	sylancr 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
78		eleq1 2259	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹‘𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛))))
79	78	spcegv 2852	. . . . . . . . . 10 ⊢ (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
80	77, 77, 79	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
81	73, 80	exlimddv 1913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
82	28	eleq2d 2266	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑤 ∈ (𝐴‘𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
83	82	exbidv 1839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴‘𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
84	81, 83	mpbird 167	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
85	64, 68, 84	syl2anc 411	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
86		simprr 531	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑧 = (𝐴‘𝑛))
87	86	eleq2d 2266	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐴‘𝑛)))
88	87	exbidv 1839	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (∃𝑤 𝑤 ∈ 𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴‘𝑛)))
89	85, 88	mpbird 167	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ 𝑧)
90	63, 89	rexlimddv 2619	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤 ∈ 𝑧)
91	90	ralrimiva 2570	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐴∃𝑤 𝑤 ∈ 𝑧)
92	1, 54, 91	ccfunen 7331	. 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧))
93		vex 2766	. . . . . . . 8 ⊢ 𝑓 ∈ V
94		funfvex 5575	. . . . . . . . . 10 ⊢ ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) → (𝐴‘𝑛) ∈ V)
95	94	funfni 5358	. . . . . . . . 9 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
96	57, 95	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
97		fvexg 5577	. . . . . . . 8 ⊢ ((𝑓 ∈ V ∧ (𝐴‘𝑛) ∈ V) → (𝑓‘(𝐴‘𝑛)) ∈ V)
98	93, 96, 97	sylancr 414	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ V)
99		2ndexg 6226	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
100	98, 99	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
101	100	ralrimiva 2570	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
102		cc2lem.g	. . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))
103	102	fnmpt 5384	. . . . 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 5558	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
108		id 19	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
109	107, 108	eleq12d 2267	. . . . . . . . 9 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
110		simplrr 536	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)
111		fnfvelrn 5694	. . . . . . . . . . 11 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
112	57, 111	sylan 283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
113	112	adantlr 477	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
114	109, 110, 113	rspcdva 2873	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
115	28	eleq2d 2266	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
116	115	adantlr 477	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
117	114, 116	mpbid 147	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)))
118		xp2nd 6224	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
119	117, 118	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
120	102	fvmpt2 5645	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛)) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
121	106, 119, 120	syl2anc 411	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
122	121, 119	eqeltrd 2273	. . . 4 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
123	122	ralrimiva 2570	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))
124	50	a1i 9	. . . . . 6 ⊢ (𝜑 → ω ∈ V)
125		fnex 5784	. . . . . 6 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126	104, 124, 125	syl2anc 411	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
127		fneq1 5346	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128		fveq1 5557	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
129	128	eleq1d 2265	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
130	129	ralbidv 2497	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
131	127, 130	anbi12d 473	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
132	131	spcegv 2852	. . . . 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 433	. 2 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
136	92, 135	exlimddv 1913	1 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364  ∃wex 1506   ∈ wcel 2167  ∀wral 2475  ∃wrex 2476  Vcvv 2763  {csn 3622  ⟨cop 3625   class class class wbr 4033   ↦ cmpt 4094  ωcom 4626   × cxp 4661  dom cdm 4663  ran crn 4664  Fun wfun 5252   Fn wfn 5253  ⟶wf 5254  –1-1→wf1 5255  –1-1-onto→wf1o 5257  ‘cfv 5258  2^nd c2nd 6197   ≈ cen 6797  CCHOICEwacc 7329

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-iinf 4624

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-2nd 6199  df-er 6592  df-en 6800  df-cc 7330

This theorem is referenced by:  cc2  7334