Theorem cc2lem 7081

Description: Lemma for cc2 7082. (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 2689	. . . . . . . 8 ⊢ 𝑛 ∈ V
3	2	snex 4109	. . . . . . 7 ⊢ {𝑛} ∈ V
4		cc2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ω)
5		funfvex 5438	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) → (𝐹‘𝑛) ∈ V)
6	5	funfni 5223	. . . . . . . 8 ⊢ ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
7	4, 6	sylan 281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐹‘𝑛) ∈ V)
8		xpexg 4653	. . . . . . 7 ⊢ (({𝑛} ∈ V ∧ (𝐹‘𝑛) ∈ V) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
9	3, 7, 8	sylancr 410	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ({𝑛} × (𝐹‘𝑛)) ∈ V)
10		cc2lem.a	. . . . . 6 ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))
11	9, 10	fmptd 5574	. . . . 5 ⊢ (𝜑 → 𝐴:ω⟶V)
12		sneq 3538	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
13		fveq2 5421	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
14	12, 13	xpeq12d 4564	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
15		simprr 521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16		vex 2689	. . . . . . . . . . 11 ⊢ 𝑘 ∈ V
17	16	snex 4109	. . . . . . . . . 10 ⊢ {𝑘} ∈ V
18	4	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19		funfvex 5438	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ V)
20	19	funfni 5223	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹‘𝑘) ∈ V)
21	18, 15, 20	syl2anc 408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹‘𝑘) ∈ V)
22		xpexg 4653	. . . . . . . . . 10 ⊢ (({𝑘} ∈ V ∧ (𝐹‘𝑘) ∈ V) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
23	17, 21, 22	sylancr 410	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹‘𝑘)) ∈ V)
24	10, 14, 15, 23	fvmptd3 5514	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑘) = ({𝑘} × (𝐹‘𝑘)))
25	24	eqeq2d 2151	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘))))
26		simpr 109	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
27	10	fvmpt2 5504	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
28	26, 9, 27	syl2anc 408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
29	28	adantrr 470	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴‘𝑛) = ({𝑛} × (𝐹‘𝑛)))
30	29	eqeq1d 2148	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴‘𝑛) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘))))
31	2	snm 3643	. . . . . . . . . 10 ⊢ ∃𝑤 𝑤 ∈ {𝑛}
32		fveq2 5421	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛))
33	32	eleq2d 2209	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑤 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑛)))
34	33	exbidv 1797	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)))
35		cc2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
36	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
37		simprl 520	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
38	34, 36, 37	rspcdva 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
39		xp11m 4977	. . . . . . . . . 10 ⊢ ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹‘𝑛)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
40	31, 38, 39	sylancr 410	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹‘𝑛) = (𝐹‘𝑘))))
41	2	sneqr 3687	. . . . . . . . . 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 2514	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))
47		dff13 5669	. . . . 5 ⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)))
48	11, 46, 47	sylanbrc 413	. . . 4 ⊢ (𝜑 → 𝐴:ω–1-1→V)
49		f1f1orn 5378	. . . . 5 ⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50		omex 4507	. . . . . 6 ⊢ ω ∈ V
51	50	f1oen 6653	. . . . 5 ⊢ (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52		ensym 6675	. . . . 5 ⊢ (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
53	49, 51, 52	3syl 17	. . . 4 ⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
54	48, 53	syl 14	. . 3 ⊢ (𝜑 → ran 𝐴 ≈ ω)
55	9	ralrimiva 2505	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V)
56	10	fnmpt 5249	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω ({𝑛} × (𝐹‘𝑛)) ∈ V → 𝐴 Fn ω)
57	55, 56	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn ω)
58	57	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59		fnfun 5220	. . . . . . 7 ⊢ (𝐴 Fn ω → Fun 𝐴)
60	58, 59	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → Fun 𝐴)
61		simpr 109	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62		elrnrexdm 5559	. . . . . 6 ⊢ (Fun 𝐴 → (𝑧 ∈ ran 𝐴 → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛)))
63	60, 61, 62	sylc 62	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴‘𝑛))
64		simpll 518	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝜑)
65		simprl 520	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ dom 𝐴)
66		fndm 5222	. . . . . . . . 9 ⊢ (𝐴 Fn ω → dom 𝐴 = ω)
67	64, 57, 66	3syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → dom 𝐴 = ω)
68	65, 67	eleqtrd 2218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑛 ∈ ω)
69	35	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))
70	34, 69, 26	rspcdva 2794	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹‘𝑛))
71		eleq1 2202	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑎 → (𝑤 ∈ (𝐹‘𝑛) ↔ 𝑎 ∈ (𝐹‘𝑛)))
72	71	cbvexv 1890	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ (𝐹‘𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
73	70, 72	sylib 121	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹‘𝑛))
74		vsnid 3557	. . . . . . . . . . 11 ⊢ 𝑛 ∈ {𝑛}
75		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → 𝑎 ∈ (𝐹‘𝑛))
76		opelxpi 4571	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
77	74, 75, 76	sylancr 410	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)))
78		eleq1 2202	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹‘𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛))))
79	78	spcegv 2774	. . . . . . . . . 10 ⊢ (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
80	77, 77, 79	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹‘𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
81	73, 80	exlimddv 1870	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛)))
82	28	eleq2d 2209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑤 ∈ (𝐴‘𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
83	82	exbidv 1797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴‘𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹‘𝑛))))
84	81, 83	mpbird 166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
85	64, 68, 84	syl2anc 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ (𝐴‘𝑛))
86		simprr 521	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → 𝑧 = (𝐴‘𝑛))
87	86	eleq2d 2209	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐴‘𝑛)))
88	87	exbidv 1797	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → (∃𝑤 𝑤 ∈ 𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴‘𝑛)))
89	85, 88	mpbird 166	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (𝐴‘𝑛))) → ∃𝑤 𝑤 ∈ 𝑧)
90	63, 89	rexlimddv 2554	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤 ∈ 𝑧)
91	90	ralrimiva 2505	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐴∃𝑤 𝑤 ∈ 𝑧)
92	1, 54, 91	ccfunen 7079	. 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧))
93		vex 2689	. . . . . . . 8 ⊢ 𝑓 ∈ V
94		funfvex 5438	. . . . . . . . . 10 ⊢ ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) → (𝐴‘𝑛) ∈ V)
95	94	funfni 5223	. . . . . . . . 9 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
96	57, 95	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ V)
97		fvexg 5440	. . . . . . . 8 ⊢ ((𝑓 ∈ V ∧ (𝐴‘𝑛) ∈ V) → (𝑓‘(𝐴‘𝑛)) ∈ V)
98	93, 96, 97	sylancr 410	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ V)
99		2ndexg 6066	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
100	98, 99	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
101	100	ralrimiva 2505	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V)
102		cc2lem.g	. . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))
103	102	fnmpt 5249	. . . . 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 5421	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛)))
108		id 19	. . . . . . . . . 10 ⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛))
109	107, 108	eleq12d 2210	. . . . . . . . 9 ⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))
110		simplrr 525	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)
111		fnfvelrn 5552	. . . . . . . . . . 11 ⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
112	57, 111	sylan 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
113	112	adantlr 468	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴)
114	109, 110, 113	rspcdva 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))
115	28	eleq2d 2209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
116	115	adantlr 468	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛))))
117	114, 116	mpbid 146	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)))
118		xp2nd 6064	. . . . . . 7 ⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐹‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
119	117, 118	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛))
120	102	fvmpt2 5504	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐹‘𝑛)) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
121	106, 119, 120	syl2anc 408	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛))))
122	121, 119	eqeltrd 2216	. . . 4 ⊢ (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺‘𝑛) ∈ (𝐹‘𝑛))
123	122	ralrimiva 2505	. . 3 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))
124	50	a1i 9	. . . . . 6 ⊢ (𝜑 → ω ∈ V)
125		fnex 5642	. . . . . 6 ⊢ ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126	104, 124, 125	syl2anc 408	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
127		fneq1 5211	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128		fveq1 5420	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛))
129	128	eleq1d 2208	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
130	129	ralbidv 2437	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛)))
131	127, 130	anbi12d 464	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺‘𝑛) ∈ (𝐹‘𝑛))))
132	131	spcegv 2774	. . . . 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 429	. 2 ⊢ ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
136	92, 135	exlimddv 1870	1 ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  Vcvv 2686  {csn 3527  ⟨cop 3530   class class class wbr 3929   ↦ cmpt 3989  ωcom 4504   × cxp 4537  dom cdm 4539  ran crn 4540  Fun wfun 5117   Fn wfn 5118  ⟶wf 5119  –1-1→wf1 5120  –1-1-onto→wf1o 5122  ‘cfv 5123  2^nd c2nd 6037   ≈ cen 6632  CCHOICEwacc 7077

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-iinf 4502

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-2nd 6039  df-er 6429  df-en 6635  df-cc 7078

This theorem is referenced by:  cc2  7082