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 10385

Description: A possibly more useful version of ax-cc 10382 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 8921	. . . 4 ⊢ Rel ≈
3	2	brrelex1i 5696	. . 3 ⊢ (𝑁 ≈ ω → 𝑁 ∈ V)
4		mptexg 7194	. . 3 ⊢ (𝑁 ∈ V → (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V)
5	1, 3, 4	mp2b 10	. 2 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) ∈ V
6		bren 8926	. . . 4 ⊢ (𝑁 ≈ ω ↔ ∃ℎ ℎ:𝑁–1-1-onto→ω)
7	1, 6	mpbi 232	. . 3 ⊢ ∃ℎ ℎ:𝑁–1-1-onto→ω
8		axcc2 10384	. . . . 5 ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
9		f1of 6795	. . . . . . . . . . 11 ⊢ (ℎ:𝑁–1-1-onto→ω → ℎ:𝑁⟶ω)
10		fnfco 6718	. . . . . . . . . . 11 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁⟶ω) → (𝑔 ∘ ℎ) Fn 𝑁)
11	9, 10	sylan2 601	. . . . . . . . . 10 ⊢ ((𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
12	11	adantlr 723	. . . . . . . . 9 ⊢ (((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
13	12	3adant1 1139	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑔 ∘ ℎ) Fn 𝑁)
14		nfmpt1 5193	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑛 ∈ 𝑁 ↦ 𝐹)
15	14	nfeq2 2935	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹)
16		nfv 1928	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))
17		nfv 1928	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ℎ:𝑁–1-1-onto→ω
18	15, 16, 17	nf3an 1915	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω)
19	9	ffvelcdmda 7054	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (ℎ‘𝑛) ∈ ω)
20		fveq2 6856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑘 ∘ ^◡ℎ)‘𝑚) = ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))
21	20	neeq1d 3010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ ↔ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅))
22		fveq2 6856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (ℎ‘𝑛) → (𝑔‘𝑚) = (𝑔‘(ℎ‘𝑛)))
23	22, 20	eleq12d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = (ℎ‘𝑛) → ((𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
24	21, 23	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = (ℎ‘𝑛) → ((((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) ↔ (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
25	24	rspcv 3572	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑛) ∈ ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
26	19, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
27	26	3ad2antl3 1197	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)))))
28		f1ocnv 6808	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω–1-1-onto→𝑁)
29		f1of 6795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡ℎ:ω–1-1-onto→𝑁 → ^◡ℎ:ω⟶𝑁)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ:𝑁–1-1-onto→ω → ^◡ℎ:ω⟶𝑁)
31		fvco3 6956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡ℎ:ω⟶𝑁 ∧ (ℎ‘𝑛) ∈ ω) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
32	30, 19, 31	syl2an2r 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
33	32	3adant1 1139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = (𝑘‘(^◡ℎ‘(ℎ‘𝑛))))
34		f1ocnvfv1 7249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (^◡ℎ‘(ℎ‘𝑛)) = 𝑛)
35	34	fveq2d 6860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
36	35	3adant1 1139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘(^◡ℎ‘(ℎ‘𝑛))) = (𝑘‘𝑛))
37		fveq1 6855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑘‘𝑛) = ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛))
38		axcc3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐹 ∈ V
39		eqid 2756	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ 𝑁 ↦ 𝐹) = (𝑛 ∈ 𝑁 ↦ 𝐹)
40	39	fvmpt2 6976	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝑁 ∧ 𝐹 ∈ V) → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
41	38, 40	mpan2 699	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑁 → ((𝑛 ∈ 𝑁 ↦ 𝐹)‘𝑛) = 𝐹)
42	37, 41	sylan9eq 2811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
43	42	3adant2 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → (𝑘‘𝑛) = 𝐹)
44	33, 36, 43	3eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
45	44	3expa 1127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
46	45	3adantl2 1177	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) = 𝐹)
47	46	neeq1d 3010	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ ↔ 𝐹 ≠ ∅))
48	9	3ad2ant3 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → ℎ:𝑁⟶ω)
49		fvco3 6956	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:𝑁⟶ω ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
50	48, 49	sylan 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔 ∘ ℎ)‘𝑛) = (𝑔‘(ℎ‘𝑛)))
51	50	eleq1d 2841	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))))
52	46	eleq2d 2842	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (((𝑔 ∘ ℎ)‘𝑛) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
53	51, 52	bitr3d 283	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
54	47, 53	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → ((((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛)) ≠ ∅ → (𝑔‘(ℎ‘𝑛)) ∈ ((𝑘 ∘ ^◡ℎ)‘(ℎ‘𝑛))) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
55	27, 54	sylibd 241	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) ∧ 𝑛 ∈ 𝑁) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
56	55	ex 415	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ 𝑔 Fn ω ∧ ℎ:𝑁–1-1-onto→ω) → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
58	57	3exp 1128	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (ℎ:𝑁–1-1-onto→ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
59	58	com34 91	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (𝑔 Fn ω → (∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))))
60	59	imp32 421	. . . . . . . . . 10 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚)))) → (ℎ:𝑁–1-1-onto→ω → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
61	60	3impia 1126	. . . . . . . . 9 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → (𝑛 ∈ 𝑁 → (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
62	18, 61	ralrimi 3254	. . . . . . . 8 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
63		vex 3452	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
64		vex 3452	. . . . . . . . . 10 ⊢ ℎ ∈ V
65	63, 64	coex 7900	. . . . . . . . 9 ⊢ (𝑔 ∘ ℎ) ∈ V
66		fneq1 6601	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓 Fn 𝑁 ↔ (𝑔 ∘ ℎ) Fn 𝑁))
67		fveq1 6855	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (𝑓‘𝑛) = ((𝑔 ∘ ℎ)‘𝑛))
68	67	eleq1d 2841	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓‘𝑛) ∈ 𝐹 ↔ ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))
69	68	imbi2d 342	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
70	69	ralbidv 3179	. . . . . . . . . 10 ⊢ (𝑓 = (𝑔 ∘ ℎ) → (∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹) ↔ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)))
71	66, 70	anbi12d 640	. . . . . . . . 9 ⊢ (𝑓 = (𝑔 ∘ ℎ) → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) ↔ ((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹))))
72	65, 71	spcev 3560	. . . . . . . 8 ⊢ (((𝑔 ∘ ℎ) Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → ((𝑔 ∘ ℎ)‘𝑛) ∈ 𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
73	13, 62, 72	syl2anc 592	. . . . . . 7 ⊢ ((𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) ∧ ℎ:𝑁–1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
74	73	3exp 1128	. . . . . 6 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ((𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
75	74	exlimdv 1947	. . . . 5 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (((𝑘 ∘ ^◡ℎ)‘𝑚) ≠ ∅ → (𝑔‘𝑚) ∈ ((𝑘 ∘ ^◡ℎ)‘𝑚))) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))))
76	8, 75	mpi 20	. . . 4 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
77	76	exlimdv 1947	. . 3 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → (∃ℎ ℎ:𝑁–1-1-onto→ω → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))))
78	7, 77	mpi 20	. 2 ⊢ (𝑘 = (𝑛 ∈ 𝑁 ↦ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)))
79	5, 78	vtocle 3517	1 ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1095 = wceq 1554 ∃wex 1793 ∈ wcel 2136 ≠ wne 2951 ∀wral 3070 Vcvv 3448 ∅c0 4280 class class class wbr 5094 ↦ cmpt 5175 ^◡ccnv 5639 ∘ ccom 5644 Fn wfn 6505 ⟶wf 6506 –1-1-onto→wf1o 6509 ‘cfv 6510 ωcom 7835 ≈ cen 8913

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-rep 5221 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-inf2 9586 ax-cc 10382

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-ral 3071 df-rex 3081 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-om 7836 df-2nd 7960 df-er 8666 df-en 8917

This theorem is referenced by: axcc4 10386 domtriomlem 10389 ovnsubaddlem2 47093

W3C validator