nnfoctbdjlem

Description: There exists a mapping from NN 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)

	Ref	Expression
Hypotheses	nnfoctbdjlem.a	$⊢ φ \to A \subseteq ℕ$
	nnfoctbdjlem.g	$⊢ φ \to G : A \underset{1-1 onto}{⟶} X$
	nnfoctbdjlem.dj	$⊢ φ \to \underset{y \in X}{Disj} y$
	nnfoctbdjlem.f	$⊢ F = (n \in ℕ ⟼ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)))$
Assertion	nnfoctbdjlem	$⊢ φ \to \exists f (f : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} f (n))$

Proof

Step	Hyp	Ref	Expression
1		nnfoctbdjlem.a	$⊢ φ \to A \subseteq ℕ$
2		nnfoctbdjlem.g	$⊢ φ \to G : A \underset{1-1 onto}{⟶} X$
3		nnfoctbdjlem.dj	$⊢ φ \to \underset{y \in X}{Disj} y$
4		nnfoctbdjlem.f	$⊢ F = (n \in ℕ ⟼ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)))$
5		iftrue	$⊢ (n = 1 \lor \neg n - 1 \in A) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = \emptyset$
6	5	adantl	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = \emptyset$
7		0ex	$⊢ \emptyset \in V$
8	7	snid	$⊢ \emptyset \in \{\emptyset\}$
9		elun2	$⊢ \emptyset \in \{\emptyset\} \to \emptyset \in (X \cup \{\emptyset\})$
10	8 9	ax-mp	$⊢ \emptyset \in (X \cup \{\emptyset\})$
11	6 10	eqeltrdi	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in (X \cup \{\emptyset\})$
12	11	adantll	$⊢ ((φ \land n \in ℕ) \land (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in (X \cup \{\emptyset\})$
13		iffalse	$⊢ \neg (n = 1 \lor \neg n - 1 \in A) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = G (n - 1)$
14	13	adantl	$⊢ ((φ \land n \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = G (n - 1)$
15		f1of	$⊢ G : A \underset{1-1 onto}{⟶} X \to G : A ⟶ X$
16	2 15	syl	$⊢ φ \to G : A ⟶ X$
17	16	adantr	$⊢ (φ \land \neg (n = 1 \lor \neg n - 1 \in A)) \to G : A ⟶ X$
18		pm2.46	$⊢ \neg (n = 1 \lor \neg n - 1 \in A) \to \neg \neg n - 1 \in A$
19	18	notnotrd	$⊢ \neg (n = 1 \lor \neg n - 1 \in A) \to n - 1 \in A$
20	19	adantl	$⊢ (φ \land \neg (n = 1 \lor \neg n - 1 \in A)) \to n - 1 \in A$
21	17 20	ffvelrnd	$⊢ (φ \land \neg (n = 1 \lor \neg n - 1 \in A)) \to G (n - 1) \in X$
22	21	adantlr	$⊢ ((φ \land n \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to G (n - 1) \in X$
23		elun1	$⊢ G (n - 1) \in X \to G (n - 1) \in (X \cup \{\emptyset\})$
24	22 23	syl	$⊢ ((φ \land n \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to G (n - 1) \in (X \cup \{\emptyset\})$
25	14 24	eqeltrd	$⊢ ((φ \land n \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in (X \cup \{\emptyset\})$
26	12 25	pm2.61dan	$⊢ (φ \land n \in ℕ) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in (X \cup \{\emptyset\})$
27	26 4	fmptd	$⊢ φ \to F : ℕ ⟶ X \cup \{\emptyset\}$
28		simpr	$⊢ (φ \land y \in X) \to y \in X$
29		f1ofo	$⊢ G : A \underset{1-1 onto}{⟶} X \to G : A \underset{onto}{⟶} X$
30		forn	$⊢ G : A \underset{onto}{⟶} X \to ran G = X$
31	2 29 30	3syl	$⊢ φ \to ran G = X$
32	31	eqcomd	$⊢ φ \to X = ran G$
33	32	adantr	$⊢ (φ \land y \in X) \to X = ran G$
34	28 33	eleqtrd	$⊢ (φ \land y \in X) \to y \in ran G$
35	16	ffnd	$⊢ φ \to G Fn A$
36		fvelrnb	$⊢ G Fn A \to (y \in ran G \leftrightarrow \exists k \in A G (k) = y)$
37	35 36	syl	$⊢ φ \to (y \in ran G \leftrightarrow \exists k \in A G (k) = y)$
38	37	adantr	$⊢ (φ \land y \in X) \to (y \in ran G \leftrightarrow \exists k \in A G (k) = y)$
39	34 38	mpbid	$⊢ (φ \land y \in X) \to \exists k \in A G (k) = y$
40	1	sselda	$⊢ (φ \land k \in A) \to k \in ℕ$
41	40	peano2nnd	$⊢ (φ \land k \in A) \to k + 1 \in ℕ$
42	41	3adant3	$⊢ (φ \land k \in A \land G (k) = y) \to k + 1 \in ℕ$
43	4	a1i	$⊢ (φ \land k \in A) \to F = (n \in ℕ ⟼ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)))$
44		1red	$⊢ ((φ \land k \in A) \land n = k + 1) \to 1 \in ℝ$
45		1red	$⊢ (φ \land k \in A) \to 1 \in ℝ$
46	40	nnrpd	$⊢ (φ \land k \in A) \to k \in ℝ^{+}$
47	45 46	ltaddrp2d	$⊢ (φ \land k \in A) \to 1 < k + 1$
48	47	adantr	$⊢ ((φ \land k \in A) \land n = k + 1) \to 1 < k + 1$
49		id	$⊢ n = k + 1 \to n = k + 1$
50	49	eqcomd	$⊢ n = k + 1 \to k + 1 = n$
51	50	adantl	$⊢ ((φ \land k \in A) \land n = k + 1) \to k + 1 = n$
52	48 51	breqtrd	$⊢ ((φ \land k \in A) \land n = k + 1) \to 1 < n$
53	44 52	gtned	$⊢ ((φ \land k \in A) \land n = k + 1) \to n \neq 1$
54	53	neneqd	$⊢ ((φ \land k \in A) \land n = k + 1) \to \neg n = 1$
55		oveq1	$⊢ n = k + 1 \to n - 1 = k + 1 - 1$
56	40	nncnd	$⊢ (φ \land k \in A) \to k \in ℂ$
57		1cnd	$⊢ (φ \land k \in A) \to 1 \in ℂ$
58	56 57	pncand	$⊢ (φ \land k \in A) \to k + 1 - 1 = k$
59	55 58	sylan9eqr	$⊢ ((φ \land k \in A) \land n = k + 1) \to n - 1 = k$
60		simplr	$⊢ ((φ \land k \in A) \land n = k + 1) \to k \in A$
61	59 60	eqeltrd	$⊢ ((φ \land k \in A) \land n = k + 1) \to n - 1 \in A$
62	61	notnotd	$⊢ ((φ \land k \in A) \land n = k + 1) \to \neg \neg n - 1 \in A$
63		ioran	$⊢ \neg (n = 1 \lor \neg n - 1 \in A) \leftrightarrow (\neg n = 1 \land \neg \neg n - 1 \in A)$
64	54 62 63	sylanbrc	$⊢ ((φ \land k \in A) \land n = k + 1) \to \neg (n = 1 \lor \neg n - 1 \in A)$
65	64	iffalsed	$⊢ ((φ \land k \in A) \land n = k + 1) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = G (n - 1)$
66	59	fveq2d	$⊢ ((φ \land k \in A) \land n = k + 1) \to G (n - 1) = G (k)$
67	65 66	eqtrd	$⊢ ((φ \land k \in A) \land n = k + 1) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = G (k)$
68	16	ffvelrnda	$⊢ (φ \land k \in A) \to G (k) \in X$
69	43 67 41 68	fvmptd	$⊢ (φ \land k \in A) \to F (k + 1) = G (k)$
70	69	3adant3	$⊢ (φ \land k \in A \land G (k) = y) \to F (k + 1) = G (k)$
71		simp3	$⊢ (φ \land k \in A \land G (k) = y) \to G (k) = y$
72	70 71	eqtrd	$⊢ (φ \land k \in A \land G (k) = y) \to F (k + 1) = y$
73		fveq2	$⊢ m = k + 1 \to F (m) = F (k + 1)$
74	73	eqeq1d	$⊢ m = k + 1 \to (F (m) = y \leftrightarrow F (k + 1) = y)$
75	74	rspcev	$⊢ (k + 1 \in ℕ \land F (k + 1) = y) \to \exists m \in ℕ F (m) = y$
76	42 72 75	syl2anc	$⊢ (φ \land k \in A \land G (k) = y) \to \exists m \in ℕ F (m) = y$
77	76	3exp	$⊢ φ \to (k \in A \to (G (k) = y \to \exists m \in ℕ F (m) = y))$
78	77	adantr	$⊢ (φ \land y \in X) \to (k \in A \to (G (k) = y \to \exists m \in ℕ F (m) = y))$
79	78	rexlimdv	$⊢ (φ \land y \in X) \to (\exists k \in A G (k) = y \to \exists m \in ℕ F (m) = y)$
80	39 79	mpd	$⊢ (φ \land y \in X) \to \exists m \in ℕ F (m) = y$
81		id	$⊢ F (m) = y \to F (m) = y$
82	81	eqcomd	$⊢ F (m) = y \to y = F (m)$
83	82	a1i	$⊢ ((φ \land y \in X) \land m \in ℕ) \to (F (m) = y \to y = F (m))$
84	83	reximdva	$⊢ (φ \land y \in X) \to (\exists m \in ℕ F (m) = y \to \exists m \in ℕ y = F (m))$
85	80 84	mpd	$⊢ (φ \land y \in X) \to \exists m \in ℕ y = F (m)$
86	85	adantlr	$⊢ ((φ \land y \in (X \cup \{\emptyset\})) \land y \in X) \to \exists m \in ℕ y = F (m)$
87		simpll	$⊢ ((φ \land y \in (X \cup \{\emptyset\})) \land \neg y \in X) \to φ$
88		elunnel1	$⊢ (y \in (X \cup \{\emptyset\}) \land \neg y \in X) \to y \in \{\emptyset\}$
89		elsni	$⊢ y \in \{\emptyset\} \to y = \emptyset$
90	88 89	syl	$⊢ (y \in (X \cup \{\emptyset\}) \land \neg y \in X) \to y = \emptyset$
91	90	adantll	$⊢ ((φ \land y \in (X \cup \{\emptyset\})) \land \neg y \in X) \to y = \emptyset$
92		1nn	$⊢ 1 \in ℕ$
93	92	a1i	$⊢ (φ \land y = \emptyset) \to 1 \in ℕ$
94	5	orcs	$⊢ n = 1 \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = \emptyset$
95	92	a1i	$⊢ φ \to 1 \in ℕ$
96	7	a1i	$⊢ φ \to \emptyset \in V$
97	4 94 95 96	fvmptd3	$⊢ φ \to F (1) = \emptyset$
98	97	adantr	$⊢ (φ \land y = \emptyset) \to F (1) = \emptyset$
99		id	$⊢ y = \emptyset \to y = \emptyset$
100	99	eqcomd	$⊢ y = \emptyset \to \emptyset = y$
101	100	adantl	$⊢ (φ \land y = \emptyset) \to \emptyset = y$
102	98 101	eqtr2d	$⊢ (φ \land y = \emptyset) \to y = F (1)$
103		fveq2	$⊢ m = 1 \to F (m) = F (1)$
104	103	rspceeqv	$⊢ (1 \in ℕ \land y = F (1)) \to \exists m \in ℕ y = F (m)$
105	93 102 104	syl2anc	$⊢ (φ \land y = \emptyset) \to \exists m \in ℕ y = F (m)$
106	87 91 105	syl2anc	$⊢ ((φ \land y \in (X \cup \{\emptyset\})) \land \neg y \in X) \to \exists m \in ℕ y = F (m)$
107	86 106	pm2.61dan	$⊢ (φ \land y \in (X \cup \{\emptyset\})) \to \exists m \in ℕ y = F (m)$
108	107	ralrimiva	$⊢ φ \to \forall y \in (X \cup \{\emptyset\}) \exists m \in ℕ y = F (m)$
109		dffo3	$⊢ F : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \leftrightarrow (F : ℕ ⟶ X \cup \{\emptyset\} \land \forall y \in (X \cup \{\emptyset\}) \exists m \in ℕ y = F (m))$
110	27 108 109	sylanbrc	$⊢ φ \to F : ℕ \underset{onto}{⟶} X \cup \{\emptyset\}$
111		animorrl	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n = m) \to (n = m \lor F (n) \cap F (m) = \emptyset)$
112	6 7	eqeltrdi	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in V$
113	4	fvmpt2	$⊢ (n \in ℕ \land if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in V) \to F (n) = if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1))$
114	112 113	syldan	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) = if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1))$
115	114 6	eqtrd	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) = \emptyset$
116	115	ineq1d	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) \cap F (m) = \emptyset \cap F (m)$
117		0in	$⊢ \emptyset \cap F (m) = \emptyset$
118	116 117	eqtrdi	$⊢ (n \in ℕ \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
119	118	adantlr	$⊢ ((n \in ℕ \land m \in ℕ) \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
120	119	ad4ant24	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land (n = 1 \lor \neg n - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
121		eqeq1	$⊢ n = m \to (n = 1 \leftrightarrow m = 1)$
122		oveq1	$⊢ n = m \to n - 1 = m - 1$
123	122	eleq1d	$⊢ n = m \to (n - 1 \in A \leftrightarrow m - 1 \in A)$
124	123	notbid	$⊢ n = m \to (\neg n - 1 \in A \leftrightarrow \neg m - 1 \in A)$
125	121 124	orbi12d	$⊢ n = m \to ((n = 1 \lor \neg n - 1 \in A) \leftrightarrow (m = 1 \lor \neg m - 1 \in A))$
126	122	fveq2d	$⊢ n = m \to G (n - 1) = G (m - 1)$
127	125 126	ifbieq2d	$⊢ n = m \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1))$
128		simpl	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to m \in ℕ$
129		iftrue	$⊢ (m = 1 \lor \neg m - 1 \in A) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) = \emptyset$
130	129 7	eqeltrdi	$⊢ (m = 1 \lor \neg m - 1 \in A) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) \in V$
131	130	adantl	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) \in V$
132	4 127 128 131	fvmptd3	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to F (m) = if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1))$
133	129	adantl	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) = \emptyset$
134	132 133	eqtrd	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to F (m) = \emptyset$
135	134	ineq2d	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = F (n) \cap \emptyset$
136		in0	$⊢ F (n) \cap \emptyset = \emptyset$
137	135 136	eqtrdi	$⊢ (m \in ℕ \land (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
138	137	adantll	$⊢ ((n \in ℕ \land m \in ℕ) \land (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
139	138	ad5ant25	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
140		fvex	$⊢ G (n - 1) \in V$
141	7 140	ifex	$⊢ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) \in V$
142	141 113	mpan2	$⊢ n \in ℕ \to F (n) = if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1))$
143	142 13	sylan9eq	$⊢ (n \in ℕ \land \neg (n = 1 \lor \neg n - 1 \in A)) \to F (n) = G (n - 1)$
144	143	adantlr	$⊢ ((n \in ℕ \land m \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to F (n) = G (n - 1)$
145	144	3adant3	$⊢ ((n \in ℕ \land m \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (n) = G (n - 1)$
146	4	a1i	$⊢ (m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F = (n \in ℕ ⟼ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)))$
147	127	adantl	$⊢ ((m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \land n = m) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1))$
148		iffalse	$⊢ \neg (m = 1 \lor \neg m - 1 \in A) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) = G (m - 1)$
149	148	ad2antlr	$⊢ ((m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \land n = m) \to if ((m = 1 \lor \neg m - 1 \in A), \emptyset, G (m - 1)) = G (m - 1)$
150	147 149	eqtrd	$⊢ ((m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \land n = m) \to if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1)) = G (m - 1)$
151		simpl	$⊢ (m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \to m \in ℕ$
152		fvexd	$⊢ (m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (m - 1) \in V$
153	146 150 151 152	fvmptd	$⊢ (m \in ℕ \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (m) = G (m - 1)$
154	153	adantll	$⊢ ((n \in ℕ \land m \in ℕ) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (m) = G (m - 1)$
155	154	3adant2	$⊢ ((n \in ℕ \land m \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (m) = G (m - 1)$
156	145 155	ineq12d	$⊢ ((n \in ℕ \land m \in ℕ) \land \neg (n = 1 \lor \neg n - 1 \in A) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = G (n - 1) \cap G (m - 1)$
157	156	ad5ant245	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = G (n - 1) \cap G (m - 1)$
158	19	ad2antlr	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to n - 1 \in A$
159		pm2.46	$⊢ \neg (m = 1 \lor \neg m - 1 \in A) \to \neg \neg m - 1 \in A$
160	159	notnotrd	$⊢ \neg (m = 1 \lor \neg m - 1 \in A) \to m - 1 \in A$
161	160	adantl	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to m - 1 \in A$
162		f1of1	$⊢ G : A \underset{1-1 onto}{⟶} X \to G : A \underset{1-1}{⟶} X$
163	2 162	syl	$⊢ φ \to G : A \underset{1-1}{⟶} X$
164		dff14a	$⊢ G : A \underset{1-1}{⟶} X \leftrightarrow (G : A ⟶ X \land \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y)))$
165	163 164	sylib	$⊢ φ \to (G : A ⟶ X \land \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y)))$
166	165	simprd	$⊢ φ \to \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y))$
167	166	adantr	$⊢ (φ \land (n \in ℕ \land m \in ℕ)) \to \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y))$
168	167	ad3antrrr	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y))$
169	158 161 168	jca31	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to ((n - 1 \in A \land m - 1 \in A) \land \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y)))$
170		nncn	$⊢ n \in ℕ \to n \in ℂ$
171	170	adantr	$⊢ (n \in ℕ \land m \in ℕ) \to n \in ℂ$
172	171	ad2antlr	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to n \in ℂ$
173		nncn	$⊢ m \in ℕ \to m \in ℂ$
174	173	adantl	$⊢ (n \in ℕ \land m \in ℕ) \to m \in ℂ$
175	174	ad2antlr	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to m \in ℂ$
176		1cnd	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to 1 \in ℂ$
177		simpr	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to n \neq m$
178	172 175 176 177	subneintr2d	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to n - 1 \neq m - 1$
179	178	ad2antrr	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to n - 1 \neq m - 1$
180		neeq1	$⊢ x = n - 1 \to (x \neq y \leftrightarrow n - 1 \neq y)$
181		fveq2	$⊢ x = n - 1 \to G (x) = G (n - 1)$
182	181	neeq1d	$⊢ x = n - 1 \to (G (x) \neq G (y) \leftrightarrow G (n - 1) \neq G (y))$
183	180 182	imbi12d	$⊢ x = n - 1 \to ((x \neq y \to G (x) \neq G (y)) \leftrightarrow (n - 1 \neq y \to G (n - 1) \neq G (y)))$
184		neeq2	$⊢ y = m - 1 \to (n - 1 \neq y \leftrightarrow n - 1 \neq m - 1)$
185		fveq2	$⊢ y = m - 1 \to G (y) = G (m - 1)$
186	185	neeq2d	$⊢ y = m - 1 \to (G (n - 1) \neq G (y) \leftrightarrow G (n - 1) \neq G (m - 1))$
187	184 186	imbi12d	$⊢ y = m - 1 \to ((n - 1 \neq y \to G (n - 1) \neq G (y)) \leftrightarrow (n - 1 \neq m - 1 \to G (n - 1) \neq G (m - 1)))$
188	183 187	rspc2va	$⊢ ((n - 1 \in A \land m - 1 \in A) \land \forall x \in A \forall y \in A (x \neq y \to G (x) \neq G (y))) \to (n - 1 \neq m - 1 \to G (n - 1) \neq G (m - 1))$
189	169 179 188	sylc	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (n - 1) \neq G (m - 1)$
190	189	neneqd	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to \neg G (n - 1) = G (m - 1)$
191	21	ad4ant13	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (n - 1) \in X$
192	16	ffvelrnda	$⊢ (φ \land m - 1 \in A) \to G (m - 1) \in X$
193	160 192	sylan2	$⊢ (φ \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (m - 1) \in X$
194	193	ad4ant14	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (m - 1) \in X$
195		id	$⊢ y = z \to y = z$
196	195	disjor	$⊢ \underset{y \in X}{Disj} y \leftrightarrow \forall y \in X \forall z \in X (y = z \lor y \cap z = \emptyset)$
197	3 196	sylib	$⊢ φ \to \forall y \in X \forall z \in X (y = z \lor y \cap z = \emptyset)$
198	197	ad3antrrr	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to \forall y \in X \forall z \in X (y = z \lor y \cap z = \emptyset)$
199		eqeq1	$⊢ y = G (n - 1) \to (y = z \leftrightarrow G (n - 1) = z)$
200		ineq1	$⊢ y = G (n - 1) \to y \cap z = G (n - 1) \cap z$
201	200	eqeq1d	$⊢ y = G (n - 1) \to (y \cap z = \emptyset \leftrightarrow G (n - 1) \cap z = \emptyset)$
202	199 201	orbi12d	$⊢ y = G (n - 1) \to ((y = z \lor y \cap z = \emptyset) \leftrightarrow (G (n - 1) = z \lor G (n - 1) \cap z = \emptyset))$
203		eqeq2	$⊢ z = G (m - 1) \to (G (n - 1) = z \leftrightarrow G (n - 1) = G (m - 1))$
204		ineq2	$⊢ z = G (m - 1) \to G (n - 1) \cap z = G (n - 1) \cap G (m - 1)$
205	204	eqeq1d	$⊢ z = G (m - 1) \to (G (n - 1) \cap z = \emptyset \leftrightarrow G (n - 1) \cap G (m - 1) = \emptyset)$
206	203 205	orbi12d	$⊢ z = G (m - 1) \to ((G (n - 1) = z \lor G (n - 1) \cap z = \emptyset) \leftrightarrow (G (n - 1) = G (m - 1) \lor G (n - 1) \cap G (m - 1) = \emptyset))$
207	202 206	rspc2va	$⊢ ((G (n - 1) \in X \land G (m - 1) \in X) \land \forall y \in X \forall z \in X (y = z \lor y \cap z = \emptyset)) \to (G (n - 1) = G (m - 1) \lor G (n - 1) \cap G (m - 1) = \emptyset)$
208	191 194 198 207	syl21anc	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to (G (n - 1) = G (m - 1) \lor G (n - 1) \cap G (m - 1) = \emptyset)$
209	208	adantllr	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to (G (n - 1) = G (m - 1) \lor G (n - 1) \cap G (m - 1) = \emptyset)$
210		orel1	$⊢ \neg G (n - 1) = G (m - 1) \to ((G (n - 1) = G (m - 1) \lor G (n - 1) \cap G (m - 1) = \emptyset) \to G (n - 1) \cap G (m - 1) = \emptyset)$
211	190 209 210	sylc	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to G (n - 1) \cap G (m - 1) = \emptyset$
212	157 211	eqtrd	$⊢ ((((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \land \neg (m = 1 \lor \neg m - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
213	139 212	pm2.61dan	$⊢ (((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \land \neg (n = 1 \lor \neg n - 1 \in A)) \to F (n) \cap F (m) = \emptyset$
214	120 213	pm2.61dan	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to F (n) \cap F (m) = \emptyset$
215	214	olcd	$⊢ ((φ \land (n \in ℕ \land m \in ℕ)) \land n \neq m) \to (n = m \lor F (n) \cap F (m) = \emptyset)$
216	111 215	pm2.61dane	$⊢ (φ \land (n \in ℕ \land m \in ℕ)) \to (n = m \lor F (n) \cap F (m) = \emptyset)$
217	216	ralrimivva	$⊢ φ \to \forall n \in ℕ \forall m \in ℕ (n = m \lor F (n) \cap F (m) = \emptyset)$
218		fveq2	$⊢ n = m \to F (n) = F (m)$
219	218	disjor	$⊢ \underset{n \in ℕ}{Disj} F (n) \leftrightarrow \forall n \in ℕ \forall m \in ℕ (n = m \lor F (n) \cap F (m) = \emptyset)$
220	217 219	sylibr	$⊢ φ \to \underset{n \in ℕ}{Disj} F (n)$
221		nnex	$⊢ ℕ \in V$
222	221	mptex	$⊢ (n \in ℕ ⟼ if ((n = 1 \lor \neg n - 1 \in A), \emptyset, G (n - 1))) \in V$
223	4 222	eqeltri	$⊢ F \in V$
224		foeq1	$⊢ f = F \to (f : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \leftrightarrow F : ℕ \underset{onto}{⟶} X \cup \{\emptyset\})$
225		simpl	$⊢ (f = F \land n \in ℕ) \to f = F$
226	225	fveq1d	$⊢ (f = F \land n \in ℕ) \to f (n) = F (n)$
227	226	disjeq2dv	$⊢ f = F \to (\underset{n \in ℕ}{Disj} f (n) \leftrightarrow \underset{n \in ℕ}{Disj} F (n))$
228	224 227	anbi12d	$⊢ f = F \to ((f : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} f (n)) \leftrightarrow (F : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} F (n)))$
229	223 228	spcev	$⊢ (F : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} F (n)) \to \exists f (f : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} f (n))$
230	110 220 229	syl2anc	$⊢ φ \to \exists f (f : ℕ \underset{onto}{⟶} X \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} f (n))$

Metamath Proof Explorer

Theorem nnfoctbdjlem

Proof