Theorem nnfoctbdjlem 40672

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 4092	. . . . . . . 8 ⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
2	1	adantl 482	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
3		0ex 4790	. . . . . . . . 9 ⊢ ∅ ∈ V
4	3	snid 4208	. . . . . . . 8 ⊢ ∅ ∈ {∅}
5		elun2 3781	. . . . . . . 8 ⊢ (∅ ∈ {∅} → ∅ ∈ (𝑋 ∪ {∅}))
6	4, 5	ax-mp 5	. . . . . . 7 ⊢ ∅ ∈ (𝑋 ∪ {∅})
7	2, 6	syl6eqel 2709	. . . . . 6 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
8	7	adantll 750	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
9		iffalse 4095	. . . . . . 7 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
10	9	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
11		nnfoctbdjlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)
12		f1of 6137	. . . . . . . . . . 11 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴⟶𝑋)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶𝑋)
14	13	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → 𝐺:𝐴⟶𝑋)
15		pm2.46 413	. . . . . . . . . . 11 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
16	15	notnotrd 128	. . . . . . . . . 10 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → (𝑛 − 1) ∈ 𝐴)
17	16	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
18	14, 17	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
19	18	adantlr 751	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
20		elun1 3780	. . . . . . 7 ⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
21	19, 20	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅}))
22	10, 21	eqeltrd 2701	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
23	8, 22	pm2.61dan 832	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅}))
24		nnfoctbdjlem.f	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
25	23, 24	fmptd 6385	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅}))
26		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
27		f1ofo 6144	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋)
28		forn 6118	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋)
29	11, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = 𝑋)
30	29	eqcomd 2628	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ran 𝐺)
31	30	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺)
32	26, 31	eleqtrd 2703	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺)
33	13	ffnd 6046	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 Fn 𝐴)
34		fvelrnb 6243	. . . . . . . . . . 11 ⊢ (𝐺 Fn 𝐴 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
36	35	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦))
37	32, 36	mpbid 222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)
38		nnfoctbdjlem.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℕ)
39	38	sselda 3603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ)
40	39	peano2nnd 11037	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ)
41	40	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ)
42	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
43		1red 10055	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈ ℝ)
44		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ)
45	39	nnrpd 11870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ+)
46	44, 45	ltaddrp2d 11906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1))
47	46	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1))
48		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1))
49	48	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛)
50	49	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛)
51	47, 50	breqtrd 4679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛)
52	43, 51	gtned 10172	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1)
53	52	neneqd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1)
54		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1))
55	39	nncnd 11036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ)
56		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ)
57	55, 56	pncand 10393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘)
58	54, 57	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘)
59		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴)
60	58, 59	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) ∈ 𝐴)
61	60	notnotd 138	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ ¬ (𝑛 − 1) ∈ 𝐴)
62		ioran 511	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (¬ 𝑛 = 1 ∧ ¬ ¬ (𝑛 − 1) ∈ 𝐴))
63	53, 61, 62	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴))
64	63	iffalsed 4097	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1)))
65	58	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘))
66	64, 65	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘))
67	13	ffvelrnda 6359	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋)
68	42, 66, 40, 67	fvmptd 6288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
69	68	3adant3 1081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘))
70		simp3 1063	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦)
71	69, 70	eqtrd 2656	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦)
72		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1)))
73	72	eqeq1d 2624	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦))
74	73	rspcev 3309	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℕ ∧ (𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
75	41, 71, 74	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
76	75	3exp 1264	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
77	76	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)))
78	77	rexlimdv 3030	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))
79	37, 78	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)
80		id 22	. . . . . . . . . 10 ⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦)
81	80	eqcomd 2628	. . . . . . . . 9 ⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))
82	81	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)))
83	82	reximdva 3017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
84	79, 83	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
85	84	adantlr 751	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
86		simpll 790	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑)
87		elunnel1 3754	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅})
88		elsni 4194	. . . . . . . 8 ⊢ (𝑦 ∈ {∅} → 𝑦 = ∅)
89	87, 88	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
90	89	adantll 750	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅)
91		1nn 11031	. . . . . . . 8 ⊢ 1 ∈ ℕ
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 1 ∈ ℕ)
93	24	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
94	1	orcs 409	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
95	94	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 = 1) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅)
96	91	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℕ)
97	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∅ ∈ V)
98	93, 95, 96, 97	fvmptd 6288	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘1) = ∅)
99	98	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅)
100		id 22	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → 𝑦 = ∅)
101	100	eqcomd 2628	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ∅ = 𝑦)
102	101	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦)
103	99, 102	eqtr2d 2657	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1))
104		fveq2 6191	. . . . . . . . 9 ⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1))
105	104	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑚 = 1 → (𝑦 = (𝐹‘𝑚) ↔ 𝑦 = (𝐹‘1)))
106	105	rspcev 3309	. . . . . . 7 ⊢ ((1 ∈ ℕ ∧ 𝑦 = (𝐹‘1)) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
107	92, 103, 106	syl2anc 693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = ∅) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
108	86, 90, 107	syl2anc 693	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
109	85, 108	pm2.61dan 832	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
110	109	ralrimiva 2966	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))
111		dffo3 6374	. . 3 ⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)))
112	25, 110, 111	sylanbrc 698	. 2 ⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅}))
113		animorrl 508	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
114	2, 3	syl6eqel 2709	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V)
115	24	fvmpt2 6291	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
116	114, 115	syldan 487	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
117	116, 2	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅)
118	117	ineq1d 3813	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚)))
119		0in 3969	. . . . . . . . . 10 ⊢ (∅ ∩ (𝐹‘𝑚)) = ∅
120	118, 119	syl6eq 2672	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
121	120	adantlr 751	. . . . . . . 8 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
122	121	ad4ant24 1298	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
123	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
124		eqeq1 2626	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1))
125		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1))
126	125	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴))
127	126	notbid 308	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴))
128	124, 127	orbi12d 746	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)))
129	125	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
130	128, 129	ifbieq2d 4111	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
131	130	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
132		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
133		iftrue 4092	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
134	133, 3	syl6eqel 2709	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
135	134	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V)
136	123, 131, 132, 135	fvmptd 6288	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
137	133	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅)
138	136, 137	eqtrd 2656	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅)
139	138	ineq2d 3814	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅))
140		in0 3968	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∩ ∅) = ∅
141	139, 140	syl6eq 2672	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
142	141	adantll 750	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
143	142	ad5ant25 1306	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
144		fvex 6201	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘(𝑛 − 1)) ∈ V
145	3, 144	ifex 4156	. . . . . . . . . . . . . . 15 ⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V
146	145, 115	mpan2 707	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))
147	146, 9	sylan9eq 2676	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
148	147	adantlr 751	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
149	148	3adant3 1081	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1)))
150	24	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))))
151	130	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))))
152		iffalse 4095	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
153	152	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1)))
154	151, 153	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1)))
155		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ)
156		fvexd 6203	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V)
157	150, 154, 155, 156	fvmptd 6288	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
158	157	adantll 750	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
159	158	3adant2 1080	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1)))
160	149, 159	ineq12d 3815	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
161	160	ad5ant245 1307	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
162	16	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴)
163		pm2.46 413	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → ¬ ¬ (𝑚 − 1) ∈ 𝐴)
164	163	notnotrd 128	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → (𝑚 − 1) ∈ 𝐴)
165	164	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑚 − 1) ∈ 𝐴)
166		f1of1 6136	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋)
167	11, 166	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋)
168		dff14a 6527	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐴–1-1→𝑋 ↔ (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
169	167, 168	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
170	169	simprd 479	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
171	170	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
172	171	ad3antrrr 766	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))
173	162, 165, 172	jca31 557	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))))
174		nncn 11028	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
175	174	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
176	175	ad2antlr 763	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ)
177		nncn 11028	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
178	177	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
179	178	ad2antlr 763	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ)
180		1cnd 10056	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ)
181		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚)
182	176, 179, 180, 181	subneintr2d 10438	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1))
183	182	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1))
184		neeq1 2856	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦))
185		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1)))
186	185	neeq1d 2853	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))
187	184, 186	imbi12d 334	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))))
188		neeq2 2857	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1)))
189		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1)))
190	189	neeq2d 2854	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
191	188, 190	imbi12d 334	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))))
192	187, 191	rspc2va 3323	. . . . . . . . . . . 12 ⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))
193	173, 183, 192	sylc 65	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))
194	193	neneqd 2799	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))
195	18	ad4ant13 1292	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋)
196	13	ffvelrnda 6359	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 − 1) ∈ 𝐴) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
197	164, 196	sylan2 491	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
198	197	ad4ant14 1293	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋)
199		nnfoctbdjlem.dj	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)
200		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
201	200	disjor 4634	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
202	199, 201	sylib 208	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
203	202	ad3antrrr 766	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅))
204		eqeq1 2626	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧))
205		ineq1 3807	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧))
206	205	eqeq1d 2624	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))
207	204, 206	orbi12d 746	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)))
208		eqeq2 2633	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))))
209		ineq2 3808	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))))
210	209	eqeq1d 2624	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
211	208, 210	orbi12d 746	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)))
212	207, 211	rspc2va 3323	. . . . . . . . . . . 12 ⊢ ((((𝐺‘(𝑛 − 1)) ∈ 𝑋 ∧ (𝐺‘(𝑚 − 1)) ∈ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
213	195, 198, 203, 212	syl21anc 1325	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
214	213	adantllr 755	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
215		orel1 397	. . . . . . . . . 10 ⊢ (¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))
216	194, 214, 215	sylc 65	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)
217	161, 216	eqtrd 2656	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
218	143, 217	pm2.61dan 832	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
219	122, 218	pm2.61dan 832	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)
220	219	olcd 408	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
221	113, 220	pm2.61dane 2881	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
222	221	ralrimivva 2971	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
223		fveq2 6191	. . . 4 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
224	223	disjor 4634	. . 3 ⊢ (Disj 𝑛 ∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅))
225	222, 224	sylibr 224	. 2 ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛))
226		nnex 11026	. . . . 5 ⊢ ℕ ∈ V
227	226	mptex 6486	. . . 4 ⊢ (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V
228	24, 227	eqeltri 2697	. . 3 ⊢ 𝐹 ∈ V
229		foeq1 6111	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅})))
230		simpl 473	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹)
231	230	fveq1d 6193	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛))
232	231	disjeq2dv 4625	. . . 4 ⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))
233	229, 232	anbi12d 747	. . 3 ⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))))
234	228, 233	spcev 3300	. 2 ⊢ ((𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))
235	112, 225, 234	syl2anc 693	1 ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  ifcif 4086  {csn 4177  Disj wdisj 4620   class class class wbr 4653   ↦ cmpt 4729  ran crn 5115   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –onto→wfo 5886  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650  ℂcc 9934  1c1 9937   + caddc 9939   < clt 10074   − cmin 10266  ℕcn 11020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-rp 11833

This theorem is referenced by:  nnfoctbdj  40673