axcc3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axcc3		Structured version Visualization version GIF version

Theorem axcc3 10352

Description: A possibly more useful version of ax-cc 10349 using sequences 𝐹(𝑛) instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Mario Carneiro, 26-Dec-2014.)

**Hypotheses**
Ref	Expression
axcc3.1	⊢ 𝐹 ∈ V
axcc3.2	⊢ 𝑁 ≈ ω

**Assertion**
Ref	Expression
axcc3	⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Distinct variable groups: 𝑓,𝐹 𝑓,𝑁,𝑛 Allowed substitution hint: 𝐹(𝑛)

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

Step	Hyp	Ref	Expression
1		axcc3.2	. . 3 ⊢ 𝑁 ≈ ω
2		relen 8892	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 5681	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 7169	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	mp2b 10	. 2 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V
6		bren 8897	. . . 4 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	mpbi 230	. . 3 ⊢ ∃ℎ ℎ:𝑁–1-1-onto→ω
8		axcc2 10351	. . . . 5 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
9		f1of 6775	. . . . . . . . . . 11 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
10		fnfco 6700	. . . . . . . . . . 11 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
11	9, 10	sylan2 594	. . . . . . . . . 10 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
12	11	adantlr 716	. . . . . . . . 9 ⊢ (((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
13	12	3adant1 1131	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
14		nfmpt1 5198	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
15	14	nfeq2 2917	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
16		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
17		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
18	15, 16, 17	nf3an 1903	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω)
19	9	ffvelcdmda 7031	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
20		fveq2 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
21	20	neeq1d 2992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ ↔ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅))
22		fveq2 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
23	22, 20	eleq12d 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
24	21, 23	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (ℎ‘𝑛) → ((((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) ↔ (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
25	24	rspcv 3573	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑛) ∈ ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
26	19, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
27	26	3ad2antl3 1189	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
28		f1ocnv 6787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
29		f1of 6775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω⟶𝑁)
31		fvco3 6934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
32	30, 19, 31	syl2an2r 686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
33	32	3adant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
34		f1ocnvfv1 7224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
35	34	fveq2d 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
36	35	3adant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
37		fveq1 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
38		axcc3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 ∈ V
39		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
40	39	fvmpt2 6954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
41	38, 40	mpan2 692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑁 → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
42	37, 41	sylan9eq 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
43	42	3adant2 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
44	33, 36, 43	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
45	44	3expa 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
46	45	3adantl2 1169	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
47	46	neeq1d 2992	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ ↔ 𝐹 ≠ ∅))
48	9	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
49		fvco3 6934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
50	48, 49	sylan 581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
51	50	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
52	46	eleq2d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
53	51, 52	bitr3d 281	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
54	47, 53	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
55	27, 54	sylibd 239	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
56	55	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
58	57	3exp 1120	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (ℎ:𝑁–1-1-onto→ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
59	58	com34 91	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
60	59	imp32 418	. . . . . . . . . 10 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
61	60	3impia 1118	. . . . . . . . 9 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
62	18, 61	ralrimi 3235	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
63		vex 3445	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
64		vex 3445	. . . . . . . . . 10 ⊢ ℎ ∈ V
65	63, 64	coex 7874	. . . . . . . . 9 ⊢ (𝑔 ∘ ℎ) ∈ V
66		fneq1 6584	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
67		fveq1 6834	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
68	67	eleq1d 2822	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
69	68	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
70	69	ralbidv 3160	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
71	66, 70	anbi12d 633	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
72	65, 71	spcev 3561	. . . . . . . 8 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
73	13, 62, 72	syl2anc 585	. . . . . . 7 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
74	73	3exp 1120	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
75	74	exlimdv 1935	. . . . 5 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
76	8, 75	mpi 20	. . . 4 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
77	76	exlimdv 1935	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃ℎ ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
78	7, 77	mpi 20	. 2 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
79	5, 78	vtocle 3513	1 ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3441 ∅c0 4286 class class class wbr 5099 ↦ cmpt 5180 ^◡ccnv 5624 ∘ ccom 5629 Fn wfn 6488 ⟶wf 6489 –1-1-onto→wf1o 6492 ‘cfv 6493 ωcom 7810 ≈ cen 8884

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-inf2 9554 ax-cc 10349

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-om 7811 df-2nd 7936 df-er 8637 df-en 8888

This theorem is referenced by: axcc4 10353 domtriomlem 10356 ovnsubaddlem2 46851

W3C validator