cc3 - Intuitionistic Logic Explorer

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

Theorem cc3 7387

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 6838	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 4722	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 5816	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	3syl 17	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
6		bren 6842	. . . . . . 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 2206	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
13	12	mptfng 5407	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑁 𝐹 ∈ V ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
14	11, 13	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
15	14	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁)
16		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
17	16	fneq1d 5369	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛 ∈ 𝑁 ↦ 𝐹) Fn 𝑁))
18	15, 17	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → 𝑘 Fn 𝑁)
19	18	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → 𝑘 Fn 𝑁)
20		f1ocnv 5542	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
21	20	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω–1-1-onto→𝑁)
22		f1of 5529	. . . . . . . . 9 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
23	21, 22	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ^◡ℎ:ω⟶𝑁)
24		fnfco 5457	. . . . . . . 8 ⊢ ((𝑘 Fn 𝑁 ∧ ^◡ℎ:ω⟶𝑁) → (𝑘 ∘ ^◡ℎ) Fn ω)
25	19, 23, 24	syl2anc 411	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑘 ∘ ^◡ℎ) Fn ω)
26	23	ffvelcdmda 5722	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (^◡ℎ‘𝑝) ∈ 𝑁)
27		cc3.m	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
28	27	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)
29		nfcsb1v 3127	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
30	29	nfcri 2343	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
31	30	nfex 1661	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹
32		csbeq1a 3103	. . . . . . . . . . . . 13 ⊢ (𝑛 = (^◡ℎ‘𝑝) → 𝐹 = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
33	32	eleq2d 2276	. . . . . . . . . . . 12 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝑤 ∈ 𝐹 ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
34	33	exbidv 1849	. . . . . . . . . . 11 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (∃𝑤 𝑤 ∈ 𝐹 ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
35	31, 34	rspc 2872	. . . . . . . . . 10 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹 → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
36	26, 28, 35	sylc 62	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
37		fvco3 5657	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
38	23, 37	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = (𝑘‘(^◡ℎ‘𝑝)))
39		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
40	39	fveq1d 5585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)))
41	11	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)
42	29	nfel1 2360	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V
43	32	eleq1d 2275	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (^◡ℎ‘𝑝) → (𝐹 ∈ V ↔ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
44	42, 43	rspc 2872	. . . . . . . . . . . . . . 15 ⊢ ((^◡ℎ‘𝑝) ∈ 𝑁 → (∀𝑛 ∈ 𝑁 𝐹 ∈ V → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V))
45	26, 41, 44	sylc 62	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V)
46	12	fvmpts 5664	. . . . . . . . . . . . . 14 ⊢ (((^◡ℎ‘𝑝) ∈ 𝑁 ∧ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
47	26, 45, 46	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
48	40, 47	eqtrd 2239	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(^◡ℎ‘𝑝)) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
49	38, 48	eqtrd 2239	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘𝑝) = ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹)
50	49	eleq2d 2276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
51	50	exbidv 1849	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝) ↔ ∃𝑤 𝑤 ∈ ⦋(^◡ℎ‘𝑝) / 𝑛⦌𝐹))
52	36, 51	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
53	52	ralrimiva 2580	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘 ∘ ^◡ℎ)‘𝑝))
54	10, 25, 53	cc2 7386	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
55		simprl 529	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → 𝑔 Fn ω)
56		f1of 5529	. . . . . . . . . 10 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
57	56	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
58	57	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ℎ:𝑁⟶ω)
59		fnfco 5457	. . . . . . . 8 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
60	55, 58, 59	syl2anc 411	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑔 ∘ ℎ) Fn 𝑁)
61		nfv 1552	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
62		nfmpt1 4141	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
63	62	nfeq2 2361	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
64	61, 63	nfan 1589	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
65		nfv 1552	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
66	64, 65	nfan 1589	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω)
67		nfv 1552	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
68	66, 67	nfan 1589	. . . . . . . 8 ⊢ Ⅎ𝑛(((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
69		fvco3 5657	. . . . . . . . . . . . . 14 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
70	58, 69	sylan 283	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
71		fveq2 5583	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
72		fveq2 5583	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
73	71, 72	eleq12d 2277	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
74		simplrr 536	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))
75	58	ffvelcdmda 5722	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
76	73, 74, 75	rspcdva 2883	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
77	70, 76	eqeltrd 2283	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
78	23	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ^◡ℎ:ω⟶𝑁)
79		fvco3 5657	. . . . . . . . . . . . 13 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
80	78, 75, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
81	77, 80	eleqtrd 2285	. . . . . . . . . . 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 5853	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
85	82, 83, 84	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
86	85	fveq2d 5587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
87	81, 86	eleqtrd 2285	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ (𝑘‘𝑛))
88	16	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹))
89	88	fveq1d 5585	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
90	11	r19.21bi 2595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
91	90	ad5ant15 521	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → 𝐹 ∈ V)
92	12	fvmpt2 5670	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
93	83, 91, 92	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
94	89, 93	eqtrd 2239	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
95	87, 94	eleqtrd 2285	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
96	95	ex 115	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (𝑛 ∈ 𝑁 → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
97	68, 96	ralrimi 2578	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)
98		vex 2776	. . . . . . . . 9 ⊢ 𝑔 ∈ V
99		vex 2776	. . . . . . . . 9 ⊢ ℎ ∈ V
100	98, 99	coex 5233	. . . . . . . 8 ⊢ (𝑔 ∘ ℎ) ∈ V
101		fneq1 5367	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
102		fveq1 5582	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
103	102	eleq1d 2275	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
104	103	ralbidv 2507	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹 ↔ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
105	101, 104	anbi12d 473	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
106	100, 105	spcev 2869	. . . . . . 7 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
107	60, 97, 106	syl2anc 411	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
108	54, 107	exlimddv 1923	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
109	8, 108	exlimddv 1923	. . . 4 ⊢ ((𝜑 ∧ 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
110	109	expcom 116	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
111	110	vtocleg 2845	. 2 ⊢ ((𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹)))
112	5, 111	mpcom 36	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∃wex 1516 ∈ wcel 2177 ∀wral 2485 Vcvv 2773 ⦋csb 3094 class class class wbr 4047 ↦ cmpt 4109 ωcom 4642 ^◡ccnv 4678 ∘ ccom 4683 Fn wfn 5271 ⟶wf 5272 –1-1-onto→wf1o 5275 ‘cfv 5276 ≈ cen 6832 CCHOICEwacc 7381

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4163 ax-sep 4166 ax-pow 4222 ax-pr 4257 ax-un 4484 ax-iinf 4640

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3000 df-csb 3095 df-un 3171 df-in 3173 df-ss 3180 df-pw 3619 df-sn 3640 df-pr 3641 df-op 3643 df-uni 3853 df-int 3888 df-iun 3931 df-br 4048 df-opab 4110 df-mpt 4111 df-id 4344 df-iom 4643 df-xp 4685 df-rel 4686 df-cnv 4687 df-co 4688 df-dm 4689 df-rn 4690 df-res 4691 df-ima 4692 df-iota 5237 df-fun 5278 df-fn 5279 df-f 5280 df-f1 5281 df-fo 5282 df-f1o 5283 df-fv 5284 df-2nd 6234 df-er 6627 df-en 6835 df-cc 7382

This theorem is referenced by: cc4f 7388 cc4n 7390

W3C validator