cc3 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cc3		GIF version

Theorem cc3 7351

Description: Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)

**Hypotheses**
Ref	Expression
cc3.cc	⊢ (𝜑 → CCHOICE)
cc3.f	⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
cc3.m	⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
cc3.n	⊢ (𝜑 → 𝑁 ≈ ω)

**Assertion**
Ref	Expression
cc3	⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Distinct variable groups: 𝑓,𝐹 𝑤,𝐹 𝑓,𝑁,𝑛 𝑤,𝑁,𝑛 𝜑,𝑛,𝑤 Allowed substitution hints: 𝜑(𝑓) 𝐹(𝑛)

Proof of Theorem cc3 Dummy variables 𝑔 ℎ 𝑘 𝑚 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cc3.n	. . 3 ⊢ (𝜑 → 𝑁 ≈ ω)
2		relen 6812	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 4707	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 5790	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	3syl 17	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
6		bren 6815	. . . . . . 7 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	sylib 122	. . . . . 6 ⊢ (𝜑 → ∃ℎ ℎ:𝑁–1-1-onto→ω)
8	7	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃ℎ ℎ:𝑁–1-1-onto→ω)
9		cc3.cc	. . . . . . . 8 ⊢ (𝜑 → CCHOICE)
10	9	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → CCHOICE)
11		cc3.f	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
12		eqid 2196	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
13	12	mptfng 5386	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑁 𝐹 ∈ V ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
14	11, 13	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
15	14	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
16		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
17	16	fneq1d 5349	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁))
18	15, 17	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 Fn 𝑁)
19	18	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → 𝑘 Fn 𝑁)
20		f1ocnv 5520	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
21	20	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω–1-1-onto→𝑁)
22		f1of 5507	. . . . . . . . 9 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
23	21, 22	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω⟶𝑁)
24		fnfco 5435	. . . . . . . 8 ⊢ ((𝑘 Fn 𝑁 ∧ ^◡ℎ:ω⟶𝑁) → (𝑘 ∘ ^◡ℎ) Fn ω)
25	19, 23, 24	syl2anc 411	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑘 ∘ ^◡ℎ) Fn ω)
26	23	ffvelcdmda 5700	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (^◡ℎ‘𝑝) ∈ 𝑁)
27		cc3.m	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
28	27	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
29		nfcsb1v 3117	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
30	29	nfcri 2333	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
31	30	nfex 1651	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
32		csbeq1a 3093	. . . . . . . . . . . . 13 ⊢ (𝑛 = (^◡ℎ‘𝑝) → 𝐹 = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
33	32	eleq2d 2266	. . . . . . . . . . . 12 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝑤 ∈ 𝐹 ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
34	33	exbidv 1839	. . . . . . . . . . 11 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (∃𝑤 𝑤 ∈ 𝐹 ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
35	31, 34	rspc 2862	. . . . . . . . . 10 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹 → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
36	26, 28, 35	sylc 62	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
37		fvco3 5635	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
38	23, 37	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
39		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
40	39	fveq1d 5563	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)))
41	11	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
42	29	nfel1 2350	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V
43	32	eleq1d 2265	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝐹 ∈ V ↔ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
44	42, 43	rspc 2862	. . . . . . . . . . . . . . 15 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 𝐹 ∈ V → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
45	26, 41, 44	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V)
46	12	fvmpts 5642	. . . . . . . . . . . . . 14 ⊢ (((^◡ℎ‘𝑝) ∈ 𝑁 ∧ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
47	26, 45, 46	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
48	40, 47	eqtrd 2229	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
49	38, 48	eqtrd 2229	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
50	49	eleq2d 2266	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
51	50	exbidv 1839	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
52	36, 51	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
53	52	ralrimiva 2570	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
54	10, 25, 53	cc2 7350	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
55		simprl 529	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → 𝑔 Fn ω)
56		f1of 5507	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
57	56	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
58	57	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ℎ:𝑁⟶ω)
59		fnfco 5435	. . . . . . . 8 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
60	55, 58, 59	syl2anc 411	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑔 ∘ ℎ) Fn 𝑁)
61		nfv 1542	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
62		nfmpt1 4127	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
63	62	nfeq2 2351	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
64	61, 63	nfan 1579	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
65		nfv 1542	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
66	64, 65	nfan 1579	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω)
67		nfv 1542	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
68	66, 67	nfan 1579	. . . . . . . 8 ⊢ Ⅎ𝑛(((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
69		fvco3 5635	. . . . . . . . . . . . . 14 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
70	58, 69	sylan 283	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
71		fveq2 5561	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
72		fveq2 5561	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
73	71, 72	eleq12d 2267	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
74		simplrr 536	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
75	58	ffvelcdmda 5700	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
76	73, 74, 75	rspcdva 2873	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
77	70, 76	eqeltrd 2273	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
78	23	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ^◡ℎ:ω⟶𝑁)
79		fvco3 5635	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
80	78, 75, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
81	77, 80	eleqtrd 2275	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
82		simpllr 534	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ℎ:𝑁–1-1-onto→ω)
83		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑁)
84		f1ocnvfv1 5827	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
85	82, 83, 84	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
86	85	fveq2d 5565	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
87	81, 86	eleqtrd 2275	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘𝑛))
88	16	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
89	88	fveq1d 5563	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
90	11	r19.21bi 2585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
91	90	ad5ant15 521	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
92	12	fvmpt2 5648	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
93	83, 91, 92	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
94	89, 93	eqtrd 2229	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
95	87, 94	eleqtrd 2275	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
96	95	ex 115	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑛 ∈ 𝑁 → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
97	68, 96	ralrimi 2568	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
98		vex 2766	. . . . . . . . 9 ⊢ 𝑔 ∈ V
99		vex 2766	. . . . . . . . 9 ⊢ ℎ ∈ V
100	98, 99	coex 5216	. . . . . . . 8 ⊢ (𝑔 ∘ ℎ) ∈ V
101		fneq1 5347	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
102		fveq1 5560	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
103	102	eleq1d 2265	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
104	103	ralbidv 2497	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹 ↔ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
105	101, 104	anbi12d 473	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
106	100, 105	spcev 2859	. . . . . . 7 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
107	60, 97, 106	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
108	54, 107	exlimddv 1913	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
109	8, 108	exlimddv 1913	. . . 4 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
110	109	expcom 116	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
111	110	vtocleg 2835	. 2 ⊢ ((𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
112	5, 111	mpcom 36	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 ∃wex 1506 ∈ wcel 2167 ∀wral 2475 Vcvv 2763 ⦋csb 3084 class class class wbr 4034 ↦ cmpt 4095 ωcom 4627 ^◡ccnv 4663 ∘ ccom 4668 Fn wfn 5254 ⟶wf 5255 –1-1-onto→wf1o 5258 ‘cfv 5259 ≈ cen 6806 CCHOICEwacc 7345

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 4149 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-iinf 4625

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 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-id 4329 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-2nd 6208 df-er 6601 df-en 6809 df-cc 7346

This theorem is referenced by: cc4f 7352 cc4n 7354

W3C validator