cc3 - Intuitionistic Logic Explorer

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

Theorem cc3 7422

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 6861	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 4739	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 5837	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	3syl 17	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
6		bren 6865	. . . . . . 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 2209	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
13	12	mptfng 5425	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑁 𝐹 ∈ V ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
14	11, 13	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
15	14	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
16		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
17	16	fneq1d 5387	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁))
18	15, 17	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 Fn 𝑁)
19	18	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → 𝑘 Fn 𝑁)
20		f1ocnv 5561	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
21	20	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω–1-1-onto→𝑁)
22		f1of 5548	. . . . . . . . 9 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
23	21, 22	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω⟶𝑁)
24		fnfco 5476	. . . . . . . 8 ⊢ ((𝑘 Fn 𝑁 ∧ ^◡ℎ:ω⟶𝑁) → (𝑘 ∘ ^◡ℎ) Fn ω)
25	19, 23, 24	syl2anc 411	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑘 ∘ ^◡ℎ) Fn ω)
26	23	ffvelcdmda 5743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (^◡ℎ‘𝑝) ∈ 𝑁)
27		cc3.m	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
28	27	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
29		nfcsb1v 3137	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
30	29	nfcri 2346	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
31	30	nfex 1663	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
32		csbeq1a 3113	. . . . . . . . . . . . 13 ⊢ (𝑛 = (^◡ℎ‘𝑝) → 𝐹 = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
33	32	eleq2d 2279	. . . . . . . . . . . 12 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝑤 ∈ 𝐹 ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
34	33	exbidv 1851	. . . . . . . . . . 11 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (∃𝑤 𝑤 ∈ 𝐹 ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
35	31, 34	rspc 2881	. . . . . . . . . 10 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹 → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
36	26, 28, 35	sylc 62	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
37		fvco3 5678	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
38	23, 37	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
39		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
40	39	fveq1d 5605	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)))
41	11	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
42	29	nfel1 2363	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V
43	32	eleq1d 2278	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝐹 ∈ V ↔ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
44	42, 43	rspc 2881	. . . . . . . . . . . . . . 15 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 𝐹 ∈ V → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
45	26, 41, 44	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V)
46	12	fvmpts 5685	. . . . . . . . . . . . . 14 ⊢ (((^◡ℎ‘𝑝) ∈ 𝑁 ∧ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
47	26, 45, 46	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
48	40, 47	eqtrd 2242	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
49	38, 48	eqtrd 2242	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
50	49	eleq2d 2279	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
51	50	exbidv 1851	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
52	36, 51	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
53	52	ralrimiva 2583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
54	10, 25, 53	cc2 7421	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
55		simprl 529	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → 𝑔 Fn ω)
56		f1of 5548	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
57	56	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
58	57	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ℎ:𝑁⟶ω)
59		fnfco 5476	. . . . . . . 8 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
60	55, 58, 59	syl2anc 411	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑔 ∘ ℎ) Fn 𝑁)
61		nfv 1554	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
62		nfmpt1 4156	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
63	62	nfeq2 2364	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
64	61, 63	nfan 1591	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
65		nfv 1554	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
66	64, 65	nfan 1591	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω)
67		nfv 1554	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
68	66, 67	nfan 1591	. . . . . . . 8 ⊢ Ⅎ𝑛(((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
69		fvco3 5678	. . . . . . . . . . . . . 14 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
70	58, 69	sylan 283	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
71		fveq2 5603	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
72		fveq2 5603	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
73	71, 72	eleq12d 2280	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
74		simplrr 536	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
75	58	ffvelcdmda 5743	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
76	73, 74, 75	rspcdva 2892	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
77	70, 76	eqeltrd 2286	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
78	23	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ^◡ℎ:ω⟶𝑁)
79		fvco3 5678	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
80	78, 75, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
81	77, 80	eleqtrd 2288	. . . . . . . . . . 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 5874	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
85	82, 83, 84	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
86	85	fveq2d 5607	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
87	81, 86	eleqtrd 2288	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘𝑛))
88	16	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
89	88	fveq1d 5605	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
90	11	r19.21bi 2598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
91	90	ad5ant15 521	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
92	12	fvmpt2 5691	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
93	83, 91, 92	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
94	89, 93	eqtrd 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
95	87, 94	eleqtrd 2288	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
96	95	ex 115	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑛 ∈ 𝑁 → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
97	68, 96	ralrimi 2581	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
98		vex 2782	. . . . . . . . 9 ⊢ 𝑔 ∈ V
99		vex 2782	. . . . . . . . 9 ⊢ ℎ ∈ V
100	98, 99	coex 5250	. . . . . . . 8 ⊢ (𝑔 ∘ ℎ) ∈ V
101		fneq1 5385	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
102		fveq1 5602	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
103	102	eleq1d 2278	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
104	103	ralbidv 2510	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹 ↔ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
105	101, 104	anbi12d 473	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
106	100, 105	spcev 2878	. . . . . . 7 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
107	60, 97, 106	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
108	54, 107	exlimddv 1925	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
109	8, 108	exlimddv 1925	. . . 4 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
110	109	expcom 116	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
111	110	vtocleg 2854	. 2 ⊢ ((𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
112	5, 111	mpcom 36	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1375 ∃wex 1518 ∈ wcel 2180 ∀wral 2488 Vcvv 2779 ⦋csb 3104 class class class wbr 4062 ↦ cmpt 4124 ωcom 4659 ^◡ccnv 4695 ∘ ccom 4700 Fn wfn 5289 ⟶wf 5290 –1-1-onto→wf1o 5293 ‘cfv 5294 ≈ cen 6855 CCHOICEwacc 7416

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 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-iinf 4657

This theorem depends on definitions: df-bi 117 df-3an 985 df-tru 1378 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ral 2493 df-rex 2494 df-reu 2495 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-un 3181 df-in 3183 df-ss 3190 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-id 4361 df-iom 4660 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-2nd 6257 df-er 6650 df-en 6858 df-cc 7417

This theorem is referenced by: cc4f 7423 cc4n 7425

W3C validator