cc3 - Intuitionistic Logic Explorer

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

Theorem cc3 7258

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 6738	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 4666	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 5737	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	3syl 17	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
6		bren 6741	. . . . . . 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 2177	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
13	12	mptfng 5337	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑁 𝐹 ∈ V ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
14	11, 13	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
15	14	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
16		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
17	16	fneq1d 5302	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁))
18	15, 17	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 Fn 𝑁)
19	18	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → 𝑘 Fn 𝑁)
20		f1ocnv 5470	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
21	20	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω–1-1-onto→𝑁)
22		f1of 5457	. . . . . . . . 9 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
23	21, 22	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω⟶𝑁)
24		fnfco 5386	. . . . . . . 8 ⊢ ((𝑘 Fn 𝑁 ∧ ^◡ℎ:ω⟶𝑁) → (𝑘 ∘ ^◡ℎ) Fn ω)
25	19, 23, 24	syl2anc 411	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑘 ∘ ^◡ℎ) Fn ω)
26	23	ffvelcdmda 5647	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (^◡ℎ‘𝑝) ∈ 𝑁)
27		cc3.m	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
28	27	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
29		nfcsb1v 3090	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
30	29	nfcri 2313	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
31	30	nfex 1637	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
32		csbeq1a 3066	. . . . . . . . . . . . 13 ⊢ (𝑛 = (^◡ℎ‘𝑝) → 𝐹 = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
33	32	eleq2d 2247	. . . . . . . . . . . 12 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝑤 ∈ 𝐹 ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
34	33	exbidv 1825	. . . . . . . . . . 11 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (∃𝑤 𝑤 ∈ 𝐹 ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
35	31, 34	rspc 2835	. . . . . . . . . 10 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹 → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
36	26, 28, 35	sylc 62	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
37		fvco3 5583	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
38	23, 37	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
39		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
40	39	fveq1d 5513	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)))
41	11	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
42	29	nfel1 2330	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V
43	32	eleq1d 2246	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝐹 ∈ V ↔ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
44	42, 43	rspc 2835	. . . . . . . . . . . . . . 15 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 𝐹 ∈ V → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
45	26, 41, 44	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V)
46	12	fvmpts 5590	. . . . . . . . . . . . . 14 ⊢ (((^◡ℎ‘𝑝) ∈ 𝑁 ∧ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
47	26, 45, 46	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
48	40, 47	eqtrd 2210	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
49	38, 48	eqtrd 2210	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
50	49	eleq2d 2247	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
51	50	exbidv 1825	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
52	36, 51	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
53	52	ralrimiva 2550	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
54	10, 25, 53	cc2 7257	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
55		simprl 529	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → 𝑔 Fn ω)
56		f1of 5457	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
57	56	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
58	57	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ℎ:𝑁⟶ω)
59		fnfco 5386	. . . . . . . 8 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
60	55, 58, 59	syl2anc 411	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑔 ∘ ℎ) Fn 𝑁)
61		nfv 1528	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
62		nfmpt1 4093	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
63	62	nfeq2 2331	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
64	61, 63	nfan 1565	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
65		nfv 1528	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
66	64, 65	nfan 1565	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω)
67		nfv 1528	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
68	66, 67	nfan 1565	. . . . . . . 8 ⊢ Ⅎ𝑛(((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
69		fvco3 5583	. . . . . . . . . . . . . 14 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
70	58, 69	sylan 283	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
71		fveq2 5511	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
72		fveq2 5511	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
73	71, 72	eleq12d 2248	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
74		simplrr 536	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
75	58	ffvelcdmda 5647	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
76	73, 74, 75	rspcdva 2846	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
77	70, 76	eqeltrd 2254	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
78	23	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ^◡ℎ:ω⟶𝑁)
79		fvco3 5583	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
80	78, 75, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
81	77, 80	eleqtrd 2256	. . . . . . . . . . 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 5772	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
85	82, 83, 84	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
86	85	fveq2d 5515	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
87	81, 86	eleqtrd 2256	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘𝑛))
88	16	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
89	88	fveq1d 5513	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
90	11	r19.21bi 2565	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
91	90	ad5ant15 521	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
92	12	fvmpt2 5595	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
93	83, 91, 92	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
94	89, 93	eqtrd 2210	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
95	87, 94	eleqtrd 2256	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
96	95	ex 115	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑛 ∈ 𝑁 → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
97	68, 96	ralrimi 2548	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
98		vex 2740	. . . . . . . . 9 ⊢ 𝑔 ∈ V
99		vex 2740	. . . . . . . . 9 ⊢ ℎ ∈ V
100	98, 99	coex 5170	. . . . . . . 8 ⊢ (𝑔 ∘ ℎ) ∈ V
101		fneq1 5300	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
102		fveq1 5510	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
103	102	eleq1d 2246	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
104	103	ralbidv 2477	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹 ↔ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
105	101, 104	anbi12d 473	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
106	100, 105	spcev 2832	. . . . . . 7 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
107	60, 97, 106	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
108	54, 107	exlimddv 1898	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
109	8, 108	exlimddv 1898	. . . 4 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
110	109	expcom 116	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
111	110	vtocleg 2808	. 2 ⊢ ((𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
112	5, 111	mpcom 36	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ∀wral 2455 Vcvv 2737 ⦋csb 3057 class class class wbr 4000 ↦ cmpt 4061 ωcom 4586 ^◡ccnv 4622 ∘ ccom 4627 Fn wfn 5207 ⟶wf 5208 –1-1-onto→wf1o 5211 ‘cfv 5212 ≈ cen 6732 CCHOICEwacc 7252

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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-iinf 4584

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-un 3133 df-in 3135 df-ss 3142 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-id 4290 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-2nd 6136 df-er 6529 df-en 6735 df-cc 7253

This theorem is referenced by: cc4f 7259 cc4n 7261

W3C validator