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 46470

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 4531	. . . . . . . 8 ⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
2	1	adantl 481	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
3		0ex 5307	. . . . . . . . 9 ⊢ ∅ ∈ V
4	3	snid 4662	. . . . . . . 8 ⊢ ∅ ∈ {∅}
5		elun2 4183	. . . . . . . 8 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑋 ∪ {∅}))
6	4, 5	ax-mp 5	. . . . . . 7 ⊢ ∅ ∈ (𝑋 ∪ {∅})
7	2, 6	eqeltrdi 2849	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
8	7	adantll 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
9		iffalse 4534	. . . . . . 7 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
10	9	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
11		nnfoctbdjlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)
12		f1of 6848	. . . . . . . . . . 11 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴⟶𝑋)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶𝑋)
14	13	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → 𝐺:𝐴⟶𝑋)
15		pm2.46 883	. . . . . . . . . . 11 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
16	15	notnotrd 133	. . . . . . . . . 10 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → (𝑛 − 1) ∈ 𝐴)
17	16	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
18	14, 17	ffvelcdmd 7105	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
19	18	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
20		elun1 4182	. . . . . . 7 ⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
21	19, 20	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
22	10, 21	eqeltrd 2841	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
23	8, 22	pm2.61dan 813	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
24		nnfoctbdjlem.f	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
25	23, 24	fmptd 7134	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅}))
26		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
27		f1ofo 6855	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋)
28		forn 6823	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋)
29	11, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = 𝑋)
30	29	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ran 𝐺)
31	30	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺)
32	26, 31	eleqtrd 2843	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺)
33	13	ffnd 6737	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Fn 𝐴)
34		fvelrnb 6969	. . . . . . . . . . 11 ⊢ (𝐺 Fn 𝐴 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
36	35	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
37	32, 36	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)
38		nnfoctbdjlem.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℕ)
39	38	sselda 3983	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ)
40	39	peano2nnd 12283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ)
41	40	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ)
42	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
43		1red 11262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈ ℝ)
44		1red 11262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ)
45	39	nnrpd 13075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ⁺)
46	44, 45	ltaddrp2d 13111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1))
47	46	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1))
48		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
49	48	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛)
50	49	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛)
51	47, 50	breqtrd 5169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛)
52	43, 51	gtned 11396	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1)
53	52	neneqd 2945	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1)
54		oveq1 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1))
55	39	nncnd 12282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ)
56		1cnd 11256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ)
57	55, 56	pncand 11621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘)
58	54, 57	sylan9eqr 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘)
59		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴)
60	58, 59	eqeltrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) ∈ 𝐴)
61	60	notnotd 144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
62		ioran 986	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (¬ 𝑛 = 1 ∧ ¬ ¬ (𝑛 − 1) ∈ 𝐴))
63	53, 61, 62	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴))
64	63	iffalsed 4536	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
65	58	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘))
66	64, 65	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘))
67	13	ffvelcdmda 7104	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋)
68	42, 66, 40, 67	fvmptd 7023	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
69	68	3adant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
70		simp3 1139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦)
71	69, 70	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦)
72		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1)))
73	72	eqeq1d 2739	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦))
74	73	rspcev 3622	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℕ ∧ (𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
75	41, 71, 74	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
76	75	3exp 1120	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
77	76	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
78	77	rexlimdv 3153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))
79	37, 78	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
80		id 22	. . . . . . . . . 10 ⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦)
81	80	eqcomd 2743	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))
82	81	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)))
83	82	reximdva 3168	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
84	79, 83	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
85	84	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
86		simpll 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑)
87		elunnel1 4154	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅})
88		elsni 4643	. . . . . . . 8 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
89	87, 88	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
90	89	adantll 714	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
91		1nn 12277	. . . . . . . 8 ⊢ 1 ∈ ℕ
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 1 ∈ ℕ)
93	1	orcs 876	. . . . . . . . . 10 ⊢ (𝑛 = 1 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
94	91	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
95	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∅ ∈ V)
96	24, 93, 94, 95	fvmptd3 7039	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) = ∅)
97	96	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅)
98		id 22	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
99	98	eqcomd 2743	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
100	99	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦)
101	97, 100	eqtr2d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1))
102		fveq2 6906	. . . . . . . 8 ⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1))
103	102	rspceeqv 3645	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ 𝑦 = (𝐹‘1)) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
104	92, 101, 103	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
105	86, 90, 104	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
106	85, 105	pm2.61dan 813	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
107	106	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
108		dffo3 7122	. . 3 ⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
109	25, 107, 108	sylanbrc 583	. 2 ⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅}))
110		animorrl 983	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
111	2, 3	eqeltrdi 2849	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V)
112	24	fvmpt2 7027	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
113	111, 112	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
114	113, 2	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅)
115	114	ineq1d 4219	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚)))
116		0in 4397	. . . . . . . . . 10 ⊢ (∅ ∩ (𝐹‘𝑚)) = ∅
117	115, 116	eqtrdi 2793	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
118	117	adantlr 715	. . . . . . . 8 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
119	118	ad4ant24 754	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
120		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1))
121		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1))
122	121	eleq1d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴))
123	122	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴))
124	120, 123	orbi12d 919	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)))
125	121	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
126	124, 125	ifbieq2d 4552	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
127		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
128		iftrue 4531	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
129	128, 3	eqeltrdi 2849	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
130	129	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
131	24, 126, 127, 130	fvmptd3 7039	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
132	128	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
133	131, 132	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅)
134	133	ineq2d 4220	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅))
135		in0 4395	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∩ ∅) = ∅
136	134, 135	eqtrdi 2793	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
137	136	adantll 714	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
138	137	ad5ant25 762	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
139		fvex 6919	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘(𝑛 − 1)) ∈ V
140	3, 139	ifex 4576	. . . . . . . . . . . . . . 15 ⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V
141	140, 112	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
142	141, 9	sylan9eq 2797	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
143	142	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
144	143	3adant3 1133	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
145	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
146	126	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
147		iffalse 4534	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
148	147	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
149	146, 148	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1)))
150		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
151		fvexd 6921	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V)
152	145, 149, 150, 151	fvmptd 7023	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
153	152	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
154	153	3adant2 1132	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
155	144, 154	ineq12d 4221	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
156	155	ad5ant245 1363	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
157	16	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
158		pm2.46 883	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → ¬ ¬ (𝑚 − 1) ∈ 𝐴)
159	158	notnotrd 133	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → (𝑚 − 1) ∈ 𝐴)
160	159	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑚 − 1) ∈ 𝐴)
161		f1of1 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋)
162	11, 161	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋)
163		dff14a 7290	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1→𝑋 ↔ (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
164	162, 163	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
165	164	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
166	165	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
167	166	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
168	157, 160, 167	jca31 514	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
169		nncn 12274	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
170	169	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
171	170	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ)
172		nncn 12274	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
173	172	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
174	173	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ)
175		1cnd 11256	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ)
176		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚)
177	171, 174, 175, 176	subneintr2d 11666	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1))
178	177	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1))
179		neeq1 3003	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦))
180		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1)))
181	180	neeq1d 3000	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))
182	179, 181	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))))
183		neeq2 3004	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1)))
184		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1)))
185	184	neeq2d 3001	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
186	183, 185	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))))
187	182, 186	rspc2va 3634	. . . . . . . . . . . 12 ⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
188	168, 178, 187	sylc 65	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))
189	188	neneqd 2945	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
190	18	ad4ant13 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
191	13	ffvelcdmda 7104	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 − 1) ∈ 𝐴) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
192	159, 191	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
193	192	ad4ant14 752	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
194		nnfoctbdjlem.dj	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)
195		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
196	195	disjor 5125	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
197	194, 196	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
198	197	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
199		eqeq1 2741	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧))
200		ineq1 4213	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧))
201	200	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))
202	199, 201	orbi12d 919	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)))
203		eqeq2 2749	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))))
204		ineq2 4214	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
205	204	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
206	203, 205	orbi12d 919	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)))
207	202, 206	rspc2va 3634	. . . . . . . . . . . 12 ⊢ ((((𝐺‘(𝑛 − 1)) ∈ 𝑋 ∧ (𝐺‘(𝑚 − 1)) ∈ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
208	190, 193, 198, 207	syl21anc 838	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
209	208	adantllr 719	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
210		orel1 889	. . . . . . . . . 10 ⊢ (¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
211	189, 209, 210	sylc 65	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)
212	156, 211	eqtrd 2777	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
213	138, 212	pm2.61dan 813	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
214	119, 213	pm2.61dan 813	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
215	214	olcd 875	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
216	110, 215	pm2.61dane 3029	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
217	216	ralrimivva 3202	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
218		fveq2 6906	. . . 4 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
219	218	disjor 5125	. . 3 ⊢ (Disj 𝑛 ∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
220	217, 219	sylibr 234	. 2 ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛))
221		nnex 12272	. . . . 5 ⊢ ℕ ∈ V
222	221	mptex 7243	. . . 4 ⊢ (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V
223	24, 222	eqeltri 2837	. . 3 ⊢ 𝐹 ∈ V
224		foeq1 6816	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅})))
225		simpl 482	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹)
226	225	fveq1d 6908	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛))
227	226	disjeq2dv 5115	. . . 4 ⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))
228	224, 227	anbi12d 632	. . 3 ⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))))
229	223, 228	spcev 3606	. 2 ⊢ ((𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))
230	109, 220, 229	syl2anc 584	1 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 ifcif 4525 {csn 4626 Disj wdisj 5110 class class class wbr 5143 ↦ cmpt 5225 ran crn 5686 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 1c1 11156 + caddc 11158 < clt 11295 − cmin 11492 ℕcn 12266

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-rp 13035

This theorem is referenced by: nnfoctbdj 46471

W3C validator