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 10194

Description: A possibly more useful version of ax-cc 10191 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 8738	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 5643	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 7097	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	mp2b 10	. 2 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V
6		bren 8743	. . . 4 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	mpbi 229	. . 3 ⊢ ∃ℎ ℎ:𝑁–1-1-onto→ω
8		axcc2 10193	. . . . 5 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
9		f1of 6716	. . . . . . . . . . 11 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
10		fnfco 6639	. . . . . . . . . . 11 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
11	9, 10	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
12	11	adantlr 712	. . . . . . . . 9 ⊢ (((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
13	12	3adant1 1129	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
14		nfmpt1 5182	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
15	14	nfeq2 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
16		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
17		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
18	15, 16, 17	nf3an 1904	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω)
19	9	ffvelrnda 6961	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
20		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
21	20	neeq1d 3003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ ↔ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅))
22		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
23	22, 20	eleq12d 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
24	21, 23	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (ℎ‘𝑛) → ((((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) ↔ (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
25	24	rspcv 3557	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑛) ∈ ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
26	19, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
27	26	3ad2antl3 1186	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
28		f1ocnv 6728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
29		f1of 6716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω⟶𝑁)
31		fvco3 6867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
32	30, 19, 31	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
33	32	3adant1 1129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
34		f1ocnvfv1 7148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
35	34	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
36	35	3adant1 1129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
37		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
38		axcc3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 ∈ V
39		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
40	39	fvmpt2 6886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
41	38, 40	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑁 → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
42	37, 41	sylan9eq 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
43	42	3adant2 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
44	33, 36, 43	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
45	44	3expa 1117	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
46	45	3adantl2 1166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
47	46	neeq1d 3003	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ ↔ 𝐹 ≠ ∅))
48	9	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
49		fvco3 6867	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
50	48, 49	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
51	50	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
52	46	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
53	51, 52	bitr3d 280	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
54	47, 53	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
55	27, 54	sylibd 238	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
56	55	ex 413	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
58	57	3exp 1118	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (ℎ:𝑁–1-1-onto→ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
59	58	com34 91	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
60	59	imp32 419	. . . . . . . . . 10 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
61	60	3impia 1116	. . . . . . . . 9 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
62	18, 61	ralrimi 3141	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
63		vex 3436	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
64		vex 3436	. . . . . . . . . 10 ⊢ ℎ ∈ V
65	63, 64	coex 7777	. . . . . . . . 9 ⊢ (𝑔 ∘ ℎ) ∈ V
66		fneq1 6524	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
67		fveq1 6773	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
68	67	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
69	68	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
70	69	ralbidv 3112	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
71	66, 70	anbi12d 631	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
72	65, 71	spcev 3545	. . . . . . . 8 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
73	13, 62, 72	syl2anc 584	. . . . . . 7 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
74	73	3exp 1118	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
75	74	exlimdv 1936	. . . . 5 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
76	8, 75	mpi 20	. . . 4 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
77	76	exlimdv 1936	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃ℎ ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
78	7, 77	mpi 20	. 2 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
79	5, 78	vtocle 3524	1 ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 Vcvv 3432 ∅c0 4256 class class class wbr 5074 ↦ cmpt 5157 ^◡ccnv 5588 ∘ ccom 5593 Fn wfn 6428 ⟶wf 6429 –1-1-onto→wf1o 6432 ‘cfv 6433 ωcom 7712 ≈ cen 8730

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cc 10191

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-om 7713 df-2nd 7832 df-er 8498 df-en 8734

This theorem is referenced by: axcc4 10195 domtriomlem 10198 ovnsubaddlem2 44109

W3C validator