Theorem cc2lem 7207

Description: Lemma for cc2 7208. (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 2729	. . . . . . . 8 ⊢ 𝑛 ∈ V
3	2	snex 4164	. . . . . . 7 ⊢ {𝑛} ∈ V
4		cc2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ω)
5		funfvex 5503	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) → (𝐹‘𝑛) ∈ V)
6	5	funfni 5288	. . . . . . . 8 ⊢ ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
7	4, 6	sylan 281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
8		xpexg 4718	. . . . . . 7 ⊢ (({𝑛} ∈ V ∧ (𝐹‘𝑛) ∈ V) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
9	3, 7, 8	sylancr 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
10		cc2lem.a	. . . . . 6 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
11	9, 10	fmptd 5639	. . . . 5 ⊢ (𝜑 → 𝐴:ω⟶V)
12		sneq 3587	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
13		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
14	12, 13	xpeq12d 4629	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
15		simprr 522	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16		vex 2729	. . . . . . . . . . 11 ⊢ 𝑘 ∈ V
17	16	snex 4164	. . . . . . . . . 10 ⊢ {𝑘} ∈ V
18	4	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19		funfvex 5503	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ V)
20	19	funfni 5288	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹‘𝑘) ∈ V)
21	18, 15, 20	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹‘𝑘) ∈ V)
22		xpexg 4718	. . . . . . . . . 10 ⊢ (({𝑘} ∈ V ∧ (𝐹‘𝑘) ∈ V) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
23	17, 21, 22	sylancr 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
24	10, 14, 15, 23	fvmptd3 5579	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑘) = ({𝑘} × (𝐹‘𝑘)))
25	24	eqeq2d 2177	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘))))
26		simpr 109	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
27	10	fvmpt2 5569	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
28	26, 9, 27	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
29	28	adantrr 471	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
30	29	eqeq1d 2174	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘))))
31	2	snm 3696	. . . . . . . . . 10 ⊢ ∃𝑤 𝑤 ∈ {𝑛}
32		fveq2 5486	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛))
33	32	eleq2d 2236	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑤 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑛)))
34	33	exbidv 1813	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)))
35		cc2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
36	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
37		simprl 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
38	34, 36, 37	rspcdva 2835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
39		xp11m 5042	. . . . . . . . . 10 ⊢ ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
40	31, 38, 39	sylancr 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
41	2	sneqr 3740	. . . . . . . . . 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 2548	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
47		dff13 5736	. . . . 5 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
48	11, 46, 47	sylanbrc 414	. . . 4 ⊢ (𝜑 → 𝐴:ω–1-1→V)
49		f1f1orn 5443	. . . . 5 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50		omex 4570	. . . . . 6 ⊢ ω ∈ V
51	50	f1oen 6725	. . . . 5 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52		ensym 6747	. . . . 5 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
53	49, 51, 52	3syl 17	. . . 4 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
54	48, 53	syl 14	. . 3 ⊢ (𝜑 → ran 𝐴 ≈ ω)
55	9	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V)
56	10	fnmpt 5314	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V → 𝐴 Fn ω)
57	55, 56	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn ω)
58	57	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59		fnfun 5285	. . . . . . 7 ⊢ (𝐴 Fn ω → Fun 𝐴)
60	58, 59	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → Fun 𝐴)
61		simpr 109	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62		elrnrexdm 5624	. . . . . 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 5287	. . . . . . . . 9 ⊢ (𝐴 Fn ω → dom 𝐴 = ω)
67	64, 57, 66	3syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → dom 𝐴 = ω)
68	65, 67	eleqtrd 2245	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ ω)
69	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
70	34, 69, 26	rspcdva 2835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
71		eleq1 2229	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ (𝐹‘𝑛) ↔ 𝑎 ∈ (𝐹‘𝑛)))
72	71	cbvexv 1906	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ (𝐹‘𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
73	70, 72	sylib 121	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
74		vsnid 3608	. . . . . . . . . . 11 ⊢ 𝑛 ∈ {𝑛}
75		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → 𝑎 ∈ (𝐹‘𝑛))
76		opelxpi 4636	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
77	74, 75, 76	sylancr 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
78		eleq1 2229	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹‘𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛))))
79	78	spcegv 2814	. . . . . . . . . 10 ⊢ (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
80	77, 77, 79	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
81	73, 80	exlimddv 1886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
82	28	eleq2d 2236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑤 ∈ (𝐴‘𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
83	82	exbidv 1813	. . . . . . . 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 2236	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐴‘𝑛)))
88	87	exbidv 1813	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (∃𝑤 𝑤 ∈ 𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴‘𝑛)))
89	85, 88	mpbird 166	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ 𝑧)
90	63, 89	rexlimddv 2588	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤 ∈ 𝑧)
91	90	ralrimiva 2539	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐴∃𝑤 𝑤 ∈ 𝑧)
92	1, 54, 91	ccfunen 7205	. 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧))
93		vex 2729	. . . . . . . 8 ⊢ 𝑓 ∈ V
94		funfvex 5503	. . . . . . . . . 10 ⊢ ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) → (𝐴‘𝑛) ∈ V)
95	94	funfni 5288	. . . . . . . . 9 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
96	57, 95	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
97		fvexg 5505	. . . . . . . 8 ⊢ ((𝑓 ∈ V ∧ (𝐴‘𝑛) ∈ V) → (𝑓‘(𝐴‘𝑛)) ∈ V)
98	93, 96, 97	sylancr 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ V)
99		2ndexg 6136	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
100	98, 99	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
101	100	ralrimiva 2539	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
102		cc2lem.g	. . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))
103	102	fnmpt 5314	. . . . 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 5486	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
108		id 19	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
109	107, 108	eleq12d 2237	. . . . . . . . 9 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
110		simplrr 526	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)
111		fnfvelrn 5617	. . . . . . . . . . 11 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
112	57, 111	sylan 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
113	112	adantlr 469	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
114	109, 110, 113	rspcdva 2835	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
115	28	eleq2d 2236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
116	115	adantlr 469	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
117	114, 116	mpbid 146	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)))
118		xp2nd 6134	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
119	117, 118	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
120	102	fvmpt2 5569	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛)) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
121	106, 119, 120	syl2anc 409	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
122	121, 119	eqeltrd 2243	. . . 4 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
123	122	ralrimiva 2539	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))
124	50	a1i 9	. . . . . 6 ⊢ (𝜑 → ω ∈ V)
125		fnex 5707	. . . . . 6 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126	104, 124, 125	syl2anc 409	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
127		fneq1 5276	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128		fveq1 5485	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
129	128	eleq1d 2235	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
130	129	ralbidv 2466	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
131	127, 130	anbi12d 465	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
132	131	spcegv 2814	. . . . 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 1886	1 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1343  ∃wex 1480   ∈ wcel 2136  ∀wral 2444  ∃wrex 2445  Vcvv 2726  {csn 3576  ⟨cop 3579   class class class wbr 3982   ↦ cmpt 4043  ωcom 4567   × cxp 4602  dom cdm 4604  ran crn 4605  Fun wfun 5182   Fn wfn 5183  ⟶wf 5184  –1-1→wf1 5185  –1-1-onto→wf1o 5187  ‘cfv 5188  2^nd c2nd 6107   ≈ cen 6704  CCHOICEwacc 7203

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-iinf 4565

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-reu 2451  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-id 4271  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-2nd 6109  df-er 6501  df-en 6707  df-cc 7204

This theorem is referenced by:  cc2  7208