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 47169

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 4493	. . . . . . . 8 ⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
2	1	adantl 486	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
3		0ex 5270	. . . . . . . . 9 ⊢ ∅ ∈ V
4	3	snid 4628	. . . . . . . 8 ⊢ ∅ ∈ {∅}
5		elun2 4136	. . . . . . . 8 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑋 ∪ {∅}))
6	4, 5	ax-mp 5	. . . . . . 7 ⊢ ∅ ∈ (𝑋 ∪ {∅})
7	2, 6	eqeltrdi 2871	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
8	7	adantll 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
9		iffalse 4496	. . . . . . 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 6820	. . . . . . . . . . 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 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
19	18	adantlr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
20		elun1 4135	. . . . . . 7 ⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
21	19, 20	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
22	10, 21	eqeltrd 2863	. . . . 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 7109	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅}))
26		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
27		f1ofo 6828	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋)
28		forn 6795	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋)
29	11, 27, 28	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = 𝑋)
30	29	eqcomd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ran 𝐺)
31	30	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺)
32	26, 31	eleqtrd 2865	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺)
33	13	ffnd 6706	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Fn 𝐴)
34		fvelrnb 6941	. . . . . . . . . . 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 3937	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ)
40	39	peano2nnd 12245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ)
41	40	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ)
42	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
43		1red 11204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈ ℝ)
44		1red 11204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ)
45	39	nnrpd 13053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ⁺)
46	44, 45	ltaddrp2d 13089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1))
47	46	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1))
48		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
49	48	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛)
50	49	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛)
51	47, 50	breqtrd 5137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛)
52	43, 51	gtned 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1)
53	52	neneqd 2963	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1)
54		oveq1 7417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1))
55	39	nncnd 12244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ)
56		1cnd 11197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ)
57	55, 56	pncand 11565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘)
58	54, 57	sylan9eqr 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘)
59		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴)
60	58, 59	eqeltrd 2863	. . . . . . . . . . . . . . . . . . 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 4498	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
65	58	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘))
66	64, 65	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘))
67	13	ffvelcdmda 7079	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋)
68	42, 66, 40, 67	fvmptd 6997	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
69	68	3adant3 1150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
70		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦)
71	69, 70	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦)
72		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1)))
73	72	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦))
74	73	rspcev 3581	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℕ ∧ (𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
75	41, 71, 74	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
76	75	3exp 1137	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
77	76	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
78	77	rexlimdv 3164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))
79	37, 78	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
80		id 23	. . . . . . . . . 10 ⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦)
81	80	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))
82	81	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)))
83	82	reximdva 3178	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
84	79, 83	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
85	84	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
86		simpll 778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑)
87		elunnel1 4108	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅})
88		elsni 4606	. . . . . . . 8 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
89	87, 88	syl 18	. . . . . . 7 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
90	89	adantll 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
91		1nn 12239	. . . . . . . 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 7013	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) = ∅)
97	96	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅)
98		id 23	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
99	98	eqcomd 2769	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
100	99	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦)
101	97, 100	eqtr2d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1))
102		fveq2 6881	. . . . . . . 8 ⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1))
103	102	rspceeqv 3604	. . . . . . 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 3157	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
108		dffo3 7097	. . 3 ⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
109	25, 107, 108	sylanbrc 594	. 2 ⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅}))
110		animorrl 996	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
111	2, 3	eqeltrdi 2871	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V)
112	24	fvmpt2 7001	. . . . . . . . . . . . 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 2798	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅)
115	114	ineq1d 4172	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚)))
116		0in 4354	. . . . . . . . . 10 ⊢ (∅ ∩ (𝐹‘𝑚)) = ∅
117	115, 116	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
118	117	adantlr 727	. . . . . . . 8 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
119	118	ad4ant24 766	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
120		eqeq1 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1))
121		oveq1 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1))
122	121	eleq1d 2848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴))
123	122	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴))
124	120, 123	orbi12d 931	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)))
125	121	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
126	124, 125	ifbieq2d 4514	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
127		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
128		iftrue 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
129	128, 3	eqeltrdi 2871	. . . . . . . . . . . . . . 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 7013	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
132	128	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
133	131, 132	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅)
134	133	ineq2d 4173	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅))
135		in0 4352	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∩ ∅) = ∅
136	134, 135	eqtrdi 2814	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
137	136	adantll 726	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
138	137	ad5ant25 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
139		fvex 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘(𝑛 − 1)) ∈ V
140	3, 139	ifex 4538	. . . . . . . . . . . . . . 15 ⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V
141	140, 112	mpan2 703	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
142	141, 9	sylan9eq 2818	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
143	142	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
144	143	3adant3 1150	. . . . . . . . . . 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 4496	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
148	147	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
149	146, 148	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1)))
150		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
151		fvexd 6896	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V)
152	145, 149, 150, 151	fvmptd 6997	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
153	152	adantll 726	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
154	153	3adant2 1149	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
155	144, 154	ineq12d 4174	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
156	155	ad5ant245 1384	. . . . . . . . 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 6819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋)
162	11, 161	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋)
163		dff14a 7268	. . . . . . . . . . . . . . . . 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 12236	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
170	169	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
171	170	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ)
172		nncn 12236	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
173	172	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
174	173	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ)
175		1cnd 11197	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ)
176		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚)
177	171, 174, 175, 176	subneintr2d 11610	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1))
178	177	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1))
179		neeq1 3020	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦))
180		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1)))
181	180	neeq1d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))
182	179, 181	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))))
183		neeq2 3021	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1)))
184		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1)))
185	184	neeq2d 3018	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
186	183, 185	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))))
187	182, 186	rspc2va 3593	. . . . . . . . . . . 12 ⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
188	168, 178, 187	sylc 66	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))
189	188	neneqd 2963	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
190	18	ad4ant13 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
191	13	ffvelcdmda 7079	. . . . . . . . . . . . . 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 5091	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
197	194, 196	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
198	197	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
199		eqeq1 2767	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧))
200		ineq1 4166	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧))
201	200	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))
202	199, 201	orbi12d 931	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)))
203		eqeq2 2775	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))))
204		ineq2 4167	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
205	204	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
206	203, 205	orbi12d 931	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)))
207	202, 206	rspc2va 3593	. . . . . . . . . . . 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 2798	. . . . . . . 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 3045	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
217	216	ralrimivva 3208	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
218		fveq2 6881	. . . 4 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
219	218	disjor 5091	. . 3 ⊢ (Disj 𝑛 ∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
220	217, 219	sylibr 237	. 2 ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛))
221		nnex 12234	. . . . 5 ⊢ ℕ ∈ V
222	221	mptex 7221	. . . 4 ⊢ (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V
223	24, 222	eqeltri 2859	. . 3 ⊢ 𝐹 ∈ V
224		foeq1 6788	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅})))
225		simpl 487	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹)
226	225	fveq1d 6883	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛))
227	226	disjeq2dv 5081	. . . 4 ⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))
228	224, 227	anbi12d 643	. . 3 ⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))))
229	223, 228	spcev 3565	. 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 1103 = wceq 1570 ∃wex 1809 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 Vcvv 3455 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 ifcif 4487 {csn 4589 Disj wdisj 5076 class class class wbr 5109 ↦ cmpt 5192 ran crn 5662 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ℂcc 11093 1c1 11096 + caddc 11098 < clt 11238 − cmin 11436 ℕcn 12228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-disj 5077 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-rp 13012

This theorem is referenced by: nnfoctbdj 47170

W3C validator