cc3 - Intuitionistic Logic Explorer

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

Theorem cc3 7628

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 7020	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 4816	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 5936	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	3syl 17	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
6		bren 7024	. . . . . . 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 492	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → CCHOICE)
11		cc3.f	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
12		eqid 2238	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
13	12	mptfng 5507	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑁 𝐹 ∈ V ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
14	11, 13	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
15	14	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
16		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
17	16	fneq1d 5469	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁))
18	15, 17	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 Fn 𝑁)
19	18	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → 𝑘 Fn 𝑁)
20		f1ocnv 5650	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
21	20	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω–1-1-onto→𝑁)
22		f1of 5637	. . . . . . . . 9 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
23	21, 22	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω⟶𝑁)
24		fnfco 5562	. . . . . . . 8 ⊢ ((𝑘 Fn 𝑁 ∧ ^◡ℎ:ω⟶𝑁) → (𝑘 ∘ ^◡ℎ) Fn ω)
25	19, 23, 24	syl2anc 415	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑘 ∘ ^◡ℎ) Fn ω)
26	23	ffvelcdmda 5837	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (^◡ℎ‘𝑝) ∈ 𝑁)
27		cc3.m	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
28	27	ad3antrrr 496	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
29		nfcsb1v 3180	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
30	29	nfcri 2386	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
31	30	nfex 1690	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
32		csbeq1a 3156	. . . . . . . . . . . . 13 ⊢ (𝑛 = (^◡ℎ‘𝑝) → 𝐹 = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
33	32	eleq2d 2308	. . . . . . . . . . . 12 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝑤 ∈ 𝐹 ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
34	33	exbidv 1878	. . . . . . . . . . 11 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (∃𝑤 𝑤 ∈ 𝐹 ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
35	31, 34	rspc 2923	. . . . . . . . . 10 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹 → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
36	26, 28, 35	sylc 62	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
37		fvco3 5773	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
38	23, 37	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
39		simpllr 540	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
40	39	fveq1d 5695	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)))
41	11	ad3antrrr 496	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
42	29	nfel1 2403	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V
43	32	eleq1d 2307	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝐹 ∈ V ↔ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
44	42, 43	rspc 2923	. . . . . . . . . . . . . . 15 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 𝐹 ∈ V → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
45	26, 41, 44	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V)
46	12	fvmpts 5780	. . . . . . . . . . . . . 14 ⊢ (((^◡ℎ‘𝑝) ∈ 𝑁 ∧ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
47	26, 45, 46	syl2anc 415	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
48	40, 47	eqtrd 2271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
49	38, 48	eqtrd 2271	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
50	49	eleq2d 2308	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
51	50	exbidv 1878	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
52	36, 51	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
53	52	ralrimiva 2623	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
54	10, 25, 53	cc2 7627	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
55		simprl 535	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → 𝑔 Fn ω)
56		f1of 5637	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
57	56	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
58	57	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ℎ:𝑁⟶ω)
59		fnfco 5562	. . . . . . . 8 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
60	55, 58, 59	syl2anc 415	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑔 ∘ ℎ) Fn 𝑁)
61		nfv 1581	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
62		nfmpt1 4222	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
63	62	nfeq2 2404	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
64	61, 63	nfan 1618	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
65		nfv 1581	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
66	64, 65	nfan 1618	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω)
67		nfv 1581	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
68	66, 67	nfan 1618	. . . . . . . 8 ⊢ Ⅎ𝑛(((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
69		fvco3 5773	. . . . . . . . . . . . . 14 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
70	58, 69	sylan 283	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
71		fveq2 5693	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
72		fveq2 5693	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
73	71, 72	eleq12d 2309	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
74		simplrr 542	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
75	58	ffvelcdmda 5837	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
76	73, 74, 75	rspcdva 2934	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
77	70, 76	eqeltrd 2315	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
78	23	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ^◡ℎ:ω⟶𝑁)
79		fvco3 5773	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
80	78, 75, 79	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
81	77, 80	eleqtrd 2317	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
82		simpllr 540	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ℎ:𝑁–1-1-onto→ω)
83		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑁)
84		f1ocnvfv1 5977	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
85	82, 83, 84	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
86	85	fveq2d 5697	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
87	81, 86	eleqtrd 2317	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘𝑛))
88	16	ad3antrrr 496	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
89	88	fveq1d 5695	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
90	11	r19.21bi 2638	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
91	90	ad5ant15 525	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
92	12	fvmpt2 5786	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
93	83, 91, 92	syl2anc 415	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
94	89, 93	eqtrd 2271	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
95	87, 94	eleqtrd 2317	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
96	95	ex 115	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑛 ∈ 𝑁 → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
97	68, 96	ralrimi 2621	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
98		vex 2824	. . . . . . . . 9 ⊢ 𝑔 ∈ V
99		vex 2824	. . . . . . . . 9 ⊢ ℎ ∈ V
100	98, 99	coex 5331	. . . . . . . 8 ⊢ (𝑔 ∘ ℎ) ∈ V
101		fneq1 5467	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
102		fveq1 5692	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
103	102	eleq1d 2307	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
104	103	ralbidv 2550	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹 ↔ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
105	101, 104	anbi12d 477	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
106	100, 105	spcev 2920	. . . . . . 7 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
107	60, 97, 106	syl2anc 415	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
108	54, 107	exlimddv 1954	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
109	8, 108	exlimddv 1954	. . . 4 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
110	109	expcom 116	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
111	110	vtocleg 2896	. 2 ⊢ ((𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
112	5, 111	mpcom 36	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1402 ∃wex 1545 ∈ wcel 2209 ∀wral 2528 Vcvv 2821 ⦋csb 3147 class class class wbr 4128 ↦ cmpt 4190 ωcom 4735 ^◡ccnv 4771 ∘ ccom 4776 Fn wfn 5370 ⟶wf 5371 –1-1-onto→wf1o 5374 ‘cfv 5375 ≈ 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: cc4f 7629 cc4n 7631

W3C validator