nnfoctbdjlem - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nnfoctbdjlem		Structured version Visualization version GIF version

Theorem nnfoctbdjlem 47060

Description: There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
nnfoctbdjlem.a	⊢ (𝜑 → 𝐴 ⊆ ℕ)
nnfoctbdjlem.g	⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)
nnfoctbdjlem.dj	⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)
nnfoctbdjlem.f	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))

**Assertion**
Ref	Expression
nnfoctbdjlem	⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))

Distinct variable groups: 𝐴,𝑛,𝑦 𝑓,𝐹,𝑛 𝑦,𝐹 𝑛,𝐺,𝑦 𝑓,𝑋,𝑛 𝑦,𝑋 𝜑,𝑛,𝑦 Allowed substitution hints: 𝜑(𝑓) 𝐴(𝑓) 𝐺(𝑓)

Proof of Theorem nnfoctbdjlem Dummy variables 𝑘 𝑥 𝑚 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 4498	. . . . . . . 8 ⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
2	1	adantl 486	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
3		0ex 5272	. . . . . . . . 9 ⊢ ∅ ∈ V
4	3	snid 4633	. . . . . . . 8 ⊢ ∅ ∈ {∅}
5		elun2 4144	. . . . . . . 8 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑋 ∪ {∅}))
6	4, 5	ax-mp 5	. . . . . . 7 ⊢ ∅ ∈ (𝑋 ∪ {∅})
7	2, 6	eqeltrdi 2877	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
8	7	adantll 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
9		iffalse 4501	. . . . . . 7 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
10	9	adantl 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
11		nnfoctbdjlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)
12		f1of 6821	. . . . . . . . . . 11 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴⟶𝑋)
13	11, 12	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶𝑋)
14	13	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → 𝐺:𝐴⟶𝑋)
15		pm2.46 895	. . . . . . . . . . 11 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
16	15	notnotrd 134	. . . . . . . . . 10 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → (𝑛 − 1) ∈ 𝐴)
17	16	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
18	14, 17	ffvelcdmd 7081	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
19	18	adantlr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
20		elun1 4143	. . . . . . 7 ⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
21	19, 20	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
22	10, 21	eqeltrd 2869	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
23	8, 22	pm2.61dan 824	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
24		nnfoctbdjlem.f	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
25	23, 24	fmptd 7110	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅}))
26		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
27		f1ofo 6829	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋)
28		forn 6796	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋)
29	11, 27, 28	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = 𝑋)
30	29	eqcomd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ran 𝐺)
31	30	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺)
32	26, 31	eleqtrd 2871	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺)
33	13	ffnd 6707	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Fn 𝐴)
34		fvelrnb 6942	. . . . . . . . . . 11 ⊢ (𝐺 Fn 𝐴 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
35	33, 34	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
36	35	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
37	32, 36	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)
38		nnfoctbdjlem.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℕ)
39	38	sselda 3945	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ)
40	39	peano2nnd 12249	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ)
41	40	3adant3 1148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ)
42	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
43		1red 11208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈ ℝ)
44		1red 11208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ)
45	39	nnrpd 13057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ⁺)
46	44, 45	ltaddrp2d 13093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1))
47	46	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1))
48		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
49	48	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛)
50	49	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛)
51	47, 50	breqtrd 5141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛)
52	43, 51	gtned 11344	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1)
53	52	neneqd 2969	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1)
54		oveq1 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1))
55	39	nncnd 12248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ)
56		1cnd 11201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ)
57	55, 56	pncand 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘)
58	54, 57	sylan9eqr 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘)
59		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴)
60	58, 59	eqeltrd 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) ∈ 𝐴)
61	60	notnotd 145	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
62		ioran 999	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (¬ 𝑛 = 1 ∧ ¬ ¬ (𝑛 − 1) ∈ 𝐴))
63	53, 61, 62	sylanbrc 594	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴))
64	63	iffalsed 4503	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
65	58	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘))
66	64, 65	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘))
67	13	ffvelcdmda 7080	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋)
68	42, 66, 40, 67	fvmptd 6998	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
69	68	3adant3 1148	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
70		simp3 1154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦)
71	69, 70	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦)
72		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1)))
73	72	eqeq1d 2771	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦))
74	73	rspcev 3590	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℕ ∧ (𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
75	41, 71, 74	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
76	75	3exp 1135	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
77	76	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
78	77	rexlimdv 3170	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))
79	37, 78	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
80		id 23	. . . . . . . . . 10 ⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦)
81	80	eqcomd 2775	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))
82	81	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)))
83	82	reximdva 3184	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
84	79, 83	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
85	84	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
86		simpll 778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑)
87		elunnel1 4116	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅})
88		elsni 4611	. . . . . . . 8 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
89	87, 88	syl 18	. . . . . . 7 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
90	89	adantll 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
91		1nn 12243	. . . . . . . 8 ⊢ 1 ∈ ℕ
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 1 ∈ ℕ)
93	1	orcs 888	. . . . . . . . . 10 ⊢ (𝑛 = 1 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
94	91	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
95	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∅ ∈ V)
96	24, 93, 94, 95	fvmptd3 7014	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) = ∅)
97	96	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅)
98		id 23	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
99	98	eqcomd 2775	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
100	99	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦)
101	97, 100	eqtr2d 2805	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1))
102		fveq2 6882	. . . . . . . 8 ⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1))
103	102	rspceeqv 3613	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ 𝑦 = (𝐹‘1)) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
104	92, 101, 103	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
105	86, 90, 104	syl2anc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
106	85, 105	pm2.61dan 824	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
107	106	ralrimiva 3163	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
108		dffo3 7098	. . 3 ⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
109	25, 107, 108	sylanbrc 594	. 2 ⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅}))
110		animorrl 996	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
111	2, 3	eqeltrdi 2877	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V)
112	24	fvmpt2 7002	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
113	111, 112	syldan 602	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
114	113, 2	eqtrd 2804	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅)
115	114	ineq1d 4180	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚)))
116		0in 4361	. . . . . . . . . 10 ⊢ (∅ ∩ (𝐹‘𝑚)) = ∅
117	115, 116	eqtrdi 2820	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
118	117	adantlr 727	. . . . . . . 8 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
119	118	ad4ant24 766	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
120		eqeq1 2773	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1))
121		oveq1 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1))
122	121	eleq1d 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴))
123	122	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴))
124	120, 123	orbi12d 931	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)))
125	121	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
126	124, 125	ifbieq2d 4519	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
127		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
128		iftrue 4498	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
129	128, 3	eqeltrdi 2877	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
130	129	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
131	24, 126, 127, 130	fvmptd3 7014	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
132	128	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
133	131, 132	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅)
134	133	ineq2d 4181	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅))
135		in0 4359	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∩ ∅) = ∅
136	134, 135	eqtrdi 2820	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
137	136	adantll 726	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
138	137	ad5ant25 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
139		fvex 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘(𝑛 − 1)) ∈ V
140	3, 139	ifex 4543	. . . . . . . . . . . . . . 15 ⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V
141	140, 112	mpan2 703	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
142	141, 9	sylan9eq 2824	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
143	142	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
144	143	3adant3 1148	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
145	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
146	126	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
147		iffalse 4501	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
148	147	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
149	146, 148	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1)))
150		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
151		fvexd 6897	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V)
152	145, 149, 150, 151	fvmptd 6998	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
153	152	adantll 726	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
154	153	3adant2 1147	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
155	144, 154	ineq12d 4182	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
156	155	ad5ant245 1382	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
157	16	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
158		pm2.46 895	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → ¬ ¬ (𝑚 − 1) ∈ 𝐴)
159	158	notnotrd 134	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → (𝑚 − 1) ∈ 𝐴)
160	159	adantl 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑚 − 1) ∈ 𝐴)
161		f1of1 6820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋)
162	11, 161	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋)
163		dff14a 7269	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1→𝑋 ↔ (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
164	162, 163	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
165	164	simprd 500	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
166	165	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
167	166	ad3antrrr 742	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
168	157, 160, 167	jca31 523	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
169		nncn 12240	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
170	169	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
171	170	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ)
172		nncn 12240	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
173	172	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
174	173	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ)
175		1cnd 11201	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ)
176		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚)
177	171, 174, 175, 176	subneintr2d 11614	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1))
178	177	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1))
179		neeq1 3026	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦))
180		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1)))
181	180	neeq1d 3023	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))
182	179, 181	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))))
183		neeq2 3027	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1)))
184		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1)))
185	184	neeq2d 3024	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
186	183, 185	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))))
187	182, 186	rspc2va 3602	. . . . . . . . . . . 12 ⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
188	168, 178, 187	sylc 66	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))
189	188	neneqd 2969	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
190	18	ad4ant13 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
191	13	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 − 1) ∈ 𝐴) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
192	159, 191	sylan2 604	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
193	192	ad4ant14 764	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
194		nnfoctbdjlem.dj	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)
195		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
196	195	disjor 5095	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
197	194, 196	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
198	197	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
199		eqeq1 2773	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧))
200		ineq1 4174	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧))
201	200	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))
202	199, 201	orbi12d 931	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)))
203		eqeq2 2781	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))))
204		ineq2 4175	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
205	204	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
206	203, 205	orbi12d 931	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)))
207	202, 206	rspc2va 3602	. . . . . . . . . . . 12 ⊢ ((((𝐺‘(𝑛 − 1)) ∈ 𝑋 ∧ (𝐺‘(𝑚 − 1)) ∈ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
208	190, 193, 198, 207	syl21anc 850	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
209	208	adantllr 731	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
210		orel1 901	. . . . . . . . . 10 ⊢ (¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
211	189, 209, 210	sylc 66	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)
212	156, 211	eqtrd 2804	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
213	138, 212	pm2.61dan 824	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
214	119, 213	pm2.61dan 824	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
215	214	olcd 887	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
216	110, 215	pm2.61dane 3051	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
217	216	ralrimivva 3214	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
218		fveq2 6882	. . . 4 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
219	218	disjor 5095	. . 3 ⊢ (Disj 𝑛 ∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
220	217, 219	sylibr 237	. 2 ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛))
221		nnex 12238	. . . . 5 ⊢ ℕ ∈ V
222	221	mptex 7222	. . . 4 ⊢ (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V
223	24, 222	eqeltri 2865	. . 3 ⊢ 𝐹 ∈ V
224		foeq1 6789	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅})))
225		simpl 487	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹)
226	225	fveq1d 6884	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛))
227	226	disjeq2dv 5085	. . . 4 ⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))
228	224, 227	anbi12d 643	. . 3 ⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))))
229	223, 228	spcev 3574	. 2 ⊢ ((𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))
230	109, 220, 229	syl2anc 595	1 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 ifcif 4492 {csn 4594 Disj wdisj 5080 class class class wbr 5113 ↦ cmpt 5196 ran crn 5663 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7411 ℂcc 11097 1c1 11100 + caddc 11102 < clt 11242 − cmin 11440 ℕcn 12232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-disj 5081 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-rp 13016

This theorem is referenced by: nnfoctbdj 47061

W3C validator