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 9658

Description: A possibly more useful version of ax-cc 9655 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 8311	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 5458	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 6810	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	mp2b 10	. 2 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V
6		bren 8315	. . . 4 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	mpbi 222	. . 3 ⊢ ∃ℎ ℎ:𝑁–1-1-onto→ω
8		axcc2 9657	. . . . 5 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
9		f1of 6444	. . . . . . . . . . 11 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
10		fnfco 6372	. . . . . . . . . . 11 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
11	9, 10	sylan2 583	. . . . . . . . . 10 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
12	11	adantlr 702	. . . . . . . . 9 ⊢ (((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
13	12	3adant1 1110	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
14		nfmpt1 5025	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
15	14	nfeq2 2948	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
16		nfv 1873	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
17		nfv 1873	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
18	15, 16, 17	nf3an 1864	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω)
19	9	ffvelrnda 6676	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
20		fveq2 6499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
21	20	neeq1d 3027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ ↔ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅))
22		fveq2 6499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
23	22, 20	eleq12d 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
24	21, 23	imbi12d 337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (ℎ‘𝑛) → ((((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) ↔ (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
25	24	rspcv 3532	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑛) ∈ ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
26	19, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
27	26	3ad2antl3 1167	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
28		f1ocnv 6456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
29		f1of 6444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω⟶𝑁)
31		fvco3 6588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
32	30, 19, 31	syl2an2r 672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
33	32	3adant1 1110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
34		f1ocnvfv1 6858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
35	34	fveq2d 6503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
36	35	3adant1 1110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
37		fveq1 6498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
38		axcc3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 ∈ V
39		eqid 2779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
40	39	fvmpt2 6605	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
41	38, 40	mpan2 678	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑁 → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
42	37, 41	sylan9eq 2835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
43	42	3adant2 1111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
44	33, 36, 43	3eqtrd 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
45	44	3expa 1098	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
46	45	3adantl2 1147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
47	46	neeq1d 3027	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ ↔ 𝐹 ≠ ∅))
48	9	3ad2ant3 1115	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
49		fvco3 6588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
50	48, 49	sylan 572	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
51	50	eleq1d 2851	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
52	46	eleq2d 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
53	51, 52	bitr3d 273	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
54	47, 53	imbi12d 337	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
55	27, 54	sylibd 231	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
56	55	ex 405	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
58	57	3exp 1099	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (ℎ:𝑁–1-1-onto→ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
59	58	com34 91	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
60	59	imp32 411	. . . . . . . . . 10 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
61	60	3impia 1097	. . . . . . . . 9 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
62	18, 61	ralrimi 3167	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
63		vex 3419	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
64		vex 3419	. . . . . . . . . 10 ⊢ ℎ ∈ V
65	63, 64	coex 7450	. . . . . . . . 9 ⊢ (𝑔 ∘ ℎ) ∈ V
66		fneq1 6277	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
67		fveq1 6498	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
68	67	eleq1d 2851	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
69	68	imbi2d 333	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
70	69	ralbidv 3148	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
71	66, 70	anbi12d 621	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
72	65, 71	spcev 3526	. . . . . . . 8 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
73	13, 62, 72	syl2anc 576	. . . . . . 7 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
74	73	3exp 1099	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
75	74	exlimdv 1892	. . . . 5 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
76	8, 75	mpi 20	. . . 4 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
77	76	exlimdv 1892	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃ℎ ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
78	7, 77	mpi 20	. 2 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
79	5, 78	vtocle 3504	1 ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∃wex 1742 ∈ wcel 2050 ≠ wne 2968 ∀wral 3089 Vcvv 3416 ∅c0 4179 class class class wbr 4929 ↦ cmpt 5008 ^◡ccnv 5406 ∘ ccom 5411 Fn wfn 6183 ⟶wf 6184 –1-1-onto→wf1o 6187 ‘cfv 6188 ωcom 7396 ≈ cen 8303

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-rep 5049 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-inf2 8898 ax-cc 9655

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-pss 3846 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-om 7397 df-2nd 7502 df-er 8089 df-en 8307

This theorem is referenced by: axcc4 9659 domtriomlem 9662 ovnsubaddlem2 42282

W3C validator