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 10017

Description: A possibly more useful version of ax-cc 10014 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 8609	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 5590	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 7015	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	mp2b 10	. 2 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V
6		bren 8614	. . . 4 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	mpbi 233	. . 3 ⊢ ∃ℎ ℎ:𝑁–1-1-onto→ω
8		axcc2 10016	. . . . 5 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
9		f1of 6639	. . . . . . . . . . 11 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
10		fnfco 6562	. . . . . . . . . . 11 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
11	9, 10	sylan2 596	. . . . . . . . . 10 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
12	11	adantlr 715	. . . . . . . . 9 ⊢ (((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
13	12	3adant1 1132	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
14		nfmpt1 5138	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
15	14	nfeq2 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
16		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
17		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
18	15, 16, 17	nf3an 1909	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω)
19	9	ffvelrnda 6882	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
20		fveq2 6695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
21	20	neeq1d 2991	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ ↔ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅))
22		fveq2 6695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
23	22, 20	eleq12d 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
24	21, 23	imbi12d 348	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (ℎ‘𝑛) → ((((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) ↔ (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
25	24	rspcv 3522	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑛) ∈ ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
26	19, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
27	26	3ad2antl3 1189	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
28		f1ocnv 6651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
29		f1of 6639	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω⟶𝑁)
31		fvco3 6788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
32	30, 19, 31	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
33	32	3adant1 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
34		f1ocnvfv1 7065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
35	34	fveq2d 6699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
36	35	3adant1 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
37		fveq1 6694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
38		axcc3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 ∈ V
39		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
40	39	fvmpt2 6807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
41	38, 40	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑁 → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
42	37, 41	sylan9eq 2791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
43	42	3adant2 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
44	33, 36, 43	3eqtrd 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
45	44	3expa 1120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
46	45	3adantl2 1169	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
47	46	neeq1d 2991	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ ↔ 𝐹 ≠ ∅))
48	9	3ad2ant3 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
49		fvco3 6788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
50	48, 49	sylan 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
51	50	eleq1d 2815	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
52	46	eleq2d 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
53	51, 52	bitr3d 284	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
54	47, 53	imbi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
55	27, 54	sylibd 242	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
56	55	ex 416	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
58	57	3exp 1121	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (ℎ:𝑁–1-1-onto→ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
59	58	com34 91	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
60	59	imp32 422	. . . . . . . . . 10 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
61	60	3impia 1119	. . . . . . . . 9 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
62	18, 61	ralrimi 3127	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
63		vex 3402	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
64		vex 3402	. . . . . . . . . 10 ⊢ ℎ ∈ V
65	63, 64	coex 7686	. . . . . . . . 9 ⊢ (𝑔 ∘ ℎ) ∈ V
66		fneq1 6448	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
67		fveq1 6694	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
68	67	eleq1d 2815	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
69	68	imbi2d 344	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
70	69	ralbidv 3108	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
71	66, 70	anbi12d 634	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
72	65, 71	spcev 3511	. . . . . . . 8 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
73	13, 62, 72	syl2anc 587	. . . . . . 7 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
74	73	3exp 1121	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
75	74	exlimdv 1941	. . . . 5 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
76	8, 75	mpi 20	. . . 4 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
77	76	exlimdv 1941	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃ℎ ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
78	7, 77	mpi 20	. 2 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
79	5, 78	vtocle 3490	1 ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∃wex 1787 ∈ wcel 2112 ≠ wne 2932 ∀wral 3051 Vcvv 3398 ∅c0 4223 class class class wbr 5039 ↦ cmpt 5120 ^◡ccnv 5535 ∘ ccom 5540 Fn wfn 6353 ⟶wf 6354 –1-1-onto→wf1o 6357 ‘cfv 6358 ωcom 7622 ≈ cen 8601

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-inf2 9234 ax-cc 10014

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-reu 3058 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-om 7623 df-2nd 7740 df-er 8369 df-en 8605

This theorem is referenced by: axcc4 10018 domtriomlem 10021 ovnsubaddlem2 43727

W3C validator