Theorem nndisjeq 4430

Description: Either two naturals are disjoint or they are the same natural. Theorem X.1.18 of [Rosser] p. 526. (Contributed by SF, 17-Jan-2015.)

Assertion

Ref	Expression
nndisjeq	⊢ ((M ∈ Nn ∧ N ∈ Nn ) → ((M ∩ N) = ∅ ∨ M = N))

Proof of Theorem nndisjeq

Dummy variables a b m n q x p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . . . . 8 ⊢ p ∈ V
2	1	elcompl 3226	. . . . . . 7 ⊢ (p ∈ ∼ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ↔ ¬ p ∈ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ))
3	1	elimak 4260	. . . . . . . . 9 ⊢ (p ∈ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ↔ ∃n ∈ Nn ⟪n, p⟫ ∈ ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ))
4		opkex 4114	. . . . . . . . . . . 12 ⊢ ⟪n, p⟫ ∈ V
5	4	elcompl 3226	. . . . . . . . . . 11 ⊢ (⟪n, p⟫ ∈ ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ↔ ¬ ⟪n, p⟫ ∈ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ))
6		elun 3221	. . . . . . . . . . . 12 ⊢ (⟪n, p⟫ ∈ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ↔ (⟪n, p⟫ ∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∨ ⟪n, p⟫ ∈ Ik ))
7		vex 2863	. . . . . . . . . . . . . . . 16 ⊢ n ∈ V
8	7, 1	ndisjrelk 4324	. . . . . . . . . . . . . . 15 ⊢ (⟪n, p⟫ ∈ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ (n ∩ p) ≠ ∅)
9	8	notbii 287	. . . . . . . . . . . . . 14 ⊢ (¬ ⟪n, p⟫ ∈ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬ (n ∩ p) ≠ ∅)
10	4	elcompl 3226	. . . . . . . . . . . . . 14 ⊢ (⟪n, p⟫ ∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ ¬ ⟪n, p⟫ ∈ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c))
11		df-ne 2519	. . . . . . . . . . . . . . 15 ⊢ ((n ∩ p) ≠ ∅ ↔ ¬ (n ∩ p) = ∅)
12	11	con2bii 322	. . . . . . . . . . . . . 14 ⊢ ((n ∩ p) = ∅ ↔ ¬ (n ∩ p) ≠ ∅)
13	9, 10, 12	3bitr4i 268	. . . . . . . . . . . . 13 ⊢ (⟪n, p⟫ ∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ (n ∩ p) = ∅)
14		opkelidkg 4275	. . . . . . . . . . . . . 14 ⊢ ((n ∈ V ∧ p ∈ V) → (⟪n, p⟫ ∈ Ik ↔ n = p))
15	7, 1, 14	mp2an 653	. . . . . . . . . . . . 13 ⊢ (⟪n, p⟫ ∈ Ik ↔ n = p)
16	13, 15	orbi12i 507	. . . . . . . . . . . 12 ⊢ ((⟪n, p⟫ ∈ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∨ ⟪n, p⟫ ∈ Ik ) ↔ ((n ∩ p) = ∅ ∨ n = p))
17		incom 3449	. . . . . . . . . . . . . 14 ⊢ (n ∩ p) = (p ∩ n)
18	17	eqeq1i 2360	. . . . . . . . . . . . 13 ⊢ ((n ∩ p) = ∅ ↔ (p ∩ n) = ∅)
19		eqcom 2355	. . . . . . . . . . . . 13 ⊢ (n = p ↔ p = n)
20	18, 19	orbi12i 507	. . . . . . . . . . . 12 ⊢ (((n ∩ p) = ∅ ∨ n = p) ↔ ((p ∩ n) = ∅ ∨ p = n))
21	6, 16, 20	3bitri 262	. . . . . . . . . . 11 ⊢ (⟪n, p⟫ ∈ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ↔ ((p ∩ n) = ∅ ∨ p = n))
22	5, 21	xchbinx 301	. . . . . . . . . 10 ⊢ (⟪n, p⟫ ∈ ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ↔ ¬ ((p ∩ n) = ∅ ∨ p = n))
23	22	rexbii 2640	. . . . . . . . 9 ⊢ (∃n ∈ Nn ⟪n, p⟫ ∈ ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ↔ ∃n ∈ Nn ¬ ((p ∩ n) = ∅ ∨ p = n))
24		rexnal 2626	. . . . . . . . 9 ⊢ (∃n ∈ Nn ¬ ((p ∩ n) = ∅ ∨ p = n) ↔ ¬ ∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n))
25	3, 23, 24	3bitri 262	. . . . . . . 8 ⊢ (p ∈ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ↔ ¬ ∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n))
26	25	con2bii 322	. . . . . . 7 ⊢ (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ¬ p ∈ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ))
27	2, 26	bitr4i 243	. . . . . 6 ⊢ (p ∈ ∼ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ↔ ∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n))
28	27	eqabi 2465	. . . . 5 ⊢ ∼ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) = {p ∣ ∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n)}
29		ssetkex 4295	. . . . . . . . . . . . 13 ⊢ Sk ∈ V
30	29	ins3kex 4309	. . . . . . . . . . . 12 ⊢ Ins3k Sk ∈ V
31	29	ins2kex 4308	. . . . . . . . . . . 12 ⊢ Ins2k Sk ∈ V
32	30, 31	inex 4106	. . . . . . . . . . 11 ⊢ ( Ins3k Sk ∩ Ins2k Sk ) ∈ V
33		1cex 4143	. . . . . . . . . . . . 13 ⊢ 1c ∈ V
34	33	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘11c ∈ V
35	34	pw1ex 4304	. . . . . . . . . . 11 ⊢ ℘1℘11c ∈ V
36	32, 35	imakex 4301	. . . . . . . . . 10 ⊢ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∈ V
37	36	complex 4105	. . . . . . . . 9 ⊢ ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∈ V
38		idkex 4315	. . . . . . . . 9 ⊢ Ik ∈ V
39	37, 38	unex 4107	. . . . . . . 8 ⊢ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ∈ V
40	39	complex 4105	. . . . . . 7 ⊢ ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) ∈ V
41		nncex 4397	. . . . . . 7 ⊢ Nn ∈ V
42	40, 41	imakex 4301	. . . . . 6 ⊢ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ∈ V
43	42	complex 4105	. . . . 5 ⊢ ∼ ( ∼ ( ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∪ Ik ) “k Nn ) ∈ V
44	28, 43	eqeltrri 2424	. . . 4 ⊢ {p ∣ ∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n)} ∈ V
45		df-0c 4378	. . . . . . . . . . 11 ⊢ 0c = {∅}
46	45	eqeq2i 2363	. . . . . . . . . 10 ⊢ (p = 0c ↔ p = {∅})
47	46	biimpi 186	. . . . . . . . 9 ⊢ (p = 0c → p = {∅})
48	47	ineq1d 3457	. . . . . . . 8 ⊢ (p = 0c → (p ∩ n) = ({∅} ∩ n))
49	48	eqeq1d 2361	. . . . . . 7 ⊢ (p = 0c → ((p ∩ n) = ∅ ↔ ({∅} ∩ n) = ∅))
50		incom 3449	. . . . . . . . 9 ⊢ ({∅} ∩ n) = (n ∩ {∅})
51	50	eqeq1i 2360	. . . . . . . 8 ⊢ (({∅} ∩ n) = ∅ ↔ (n ∩ {∅}) = ∅)
52		disjsn 3787	. . . . . . . 8 ⊢ ((n ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ n)
53	51, 52	bitri 240	. . . . . . 7 ⊢ (({∅} ∩ n) = ∅ ↔ ¬ ∅ ∈ n)
54	49, 53	syl6bb 252	. . . . . 6 ⊢ (p = 0c → ((p ∩ n) = ∅ ↔ ¬ ∅ ∈ n))
55		eqeq1 2359	. . . . . . 7 ⊢ (p = 0c → (p = n ↔ 0c = n))
56		eqcom 2355	. . . . . . 7 ⊢ (0c = n ↔ n = 0c)
57	55, 56	syl6bb 252	. . . . . 6 ⊢ (p = 0c → (p = n ↔ n = 0c))
58	54, 57	orbi12d 690	. . . . 5 ⊢ (p = 0c → (((p ∩ n) = ∅ ∨ p = n) ↔ (¬ ∅ ∈ n ∨ n = 0c)))
59	58	ralbidv 2635	. . . 4 ⊢ (p = 0c → (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ∀n ∈ Nn (¬ ∅ ∈ n ∨ n = 0c)))
60		ineq1 3451	. . . . . . . 8 ⊢ (p = m → (p ∩ n) = (m ∩ n))
61	60	eqeq1d 2361	. . . . . . 7 ⊢ (p = m → ((p ∩ n) = ∅ ↔ (m ∩ n) = ∅))
62		eqeq1 2359	. . . . . . 7 ⊢ (p = m → (p = n ↔ m = n))
63	61, 62	orbi12d 690	. . . . . 6 ⊢ (p = m → (((p ∩ n) = ∅ ∨ p = n) ↔ ((m ∩ n) = ∅ ∨ m = n)))
64	63	ralbidv 2635	. . . . 5 ⊢ (p = m → (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ∀n ∈ Nn ((m ∩ n) = ∅ ∨ m = n)))
65		ineq2 3452	. . . . . . . 8 ⊢ (n = q → (m ∩ n) = (m ∩ q))
66	65	eqeq1d 2361	. . . . . . 7 ⊢ (n = q → ((m ∩ n) = ∅ ↔ (m ∩ q) = ∅))
67		equequ2 1686	. . . . . . 7 ⊢ (n = q → (m = n ↔ m = q))
68	66, 67	orbi12d 690	. . . . . 6 ⊢ (n = q → (((m ∩ n) = ∅ ∨ m = n) ↔ ((m ∩ q) = ∅ ∨ m = q)))
69	68	cbvralv 2836	. . . . 5 ⊢ (∀n ∈ Nn ((m ∩ n) = ∅ ∨ m = n) ↔ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q))
70	64, 69	syl6bb 252	. . . 4 ⊢ (p = m → (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)))
71		ineq1 3451	. . . . . . 7 ⊢ (p = (m +c 1c) → (p ∩ n) = ((m +c 1c) ∩ n))
72	71	eqeq1d 2361	. . . . . 6 ⊢ (p = (m +c 1c) → ((p ∩ n) = ∅ ↔ ((m +c 1c) ∩ n) = ∅))
73		eqeq1 2359	. . . . . 6 ⊢ (p = (m +c 1c) → (p = n ↔ (m +c 1c) = n))
74	72, 73	orbi12d 690	. . . . 5 ⊢ (p = (m +c 1c) → (((p ∩ n) = ∅ ∨ p = n) ↔ (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n)))
75	74	ralbidv 2635	. . . 4 ⊢ (p = (m +c 1c) → (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ∀n ∈ Nn (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n)))
76		ineq1 3451	. . . . . . 7 ⊢ (p = M → (p ∩ n) = (M ∩ n))
77	76	eqeq1d 2361	. . . . . 6 ⊢ (p = M → ((p ∩ n) = ∅ ↔ (M ∩ n) = ∅))
78		eqeq1 2359	. . . . . 6 ⊢ (p = M → (p = n ↔ M = n))
79	77, 78	orbi12d 690	. . . . 5 ⊢ (p = M → (((p ∩ n) = ∅ ∨ p = n) ↔ ((M ∩ n) = ∅ ∨ M = n)))
80	79	ralbidv 2635	. . . 4 ⊢ (p = M → (∀n ∈ Nn ((p ∩ n) = ∅ ∨ p = n) ↔ ∀n ∈ Nn ((M ∩ n) = ∅ ∨ M = n)))
81		nnc0suc 4413	. . . . . . 7 ⊢ (n ∈ Nn ↔ (n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)))
82		0nelsuc 4401	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ (m +c 1c)
83		eleq2 2414	. . . . . . . . . . . . 13 ⊢ (n = (m +c 1c) → (∅ ∈ n ↔ ∅ ∈ (m +c 1c)))
84	83	biimpcd 215	. . . . . . . . . . . 12 ⊢ (∅ ∈ n → (n = (m +c 1c) → ∅ ∈ (m +c 1c)))
85	82, 84	mtoi 169	. . . . . . . . . . 11 ⊢ (∅ ∈ n → ¬ n = (m +c 1c))
86	85	adantr 451	. . . . . . . . . 10 ⊢ ((∅ ∈ n ∧ m ∈ Nn ) → ¬ n = (m +c 1c))
87	86	nrexdv 2718	. . . . . . . . 9 ⊢ (∅ ∈ n → ¬ ∃m ∈ Nn n = (m +c 1c))
88		orel2 372	. . . . . . . . 9 ⊢ (¬ ∃m ∈ Nn n = (m +c 1c) → ((n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)) → n = 0c))
89	87, 88	syl 15	. . . . . . . 8 ⊢ (∅ ∈ n → ((n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)) → n = 0c))
90	89	com12 27	. . . . . . 7 ⊢ ((n = 0c ∨ ∃m ∈ Nn n = (m +c 1c)) → (∅ ∈ n → n = 0c))
91	81, 90	sylbi 187	. . . . . 6 ⊢ (n ∈ Nn → (∅ ∈ n → n = 0c))
92		imor 401	. . . . . 6 ⊢ ((∅ ∈ n → n = 0c) ↔ (¬ ∅ ∈ n ∨ n = 0c))
93	91, 92	sylib 188	. . . . 5 ⊢ (n ∈ Nn → (¬ ∅ ∈ n ∨ n = 0c))
94	93	rgen 2680	. . . 4 ⊢ ∀n ∈ Nn (¬ ∅ ∈ n ∨ n = 0c)
95		neq0 3561	. . . . . . . . 9 ⊢ (¬ ((m +c 1c) ∩ n) = ∅ ↔ ∃a a ∈ ((m +c 1c) ∩ n))
96		elin 3220	. . . . . . . . . . 11 ⊢ (a ∈ ((m +c 1c) ∩ n) ↔ (a ∈ (m +c 1c) ∧ a ∈ n))
97		elsuc 4414	. . . . . . . . . . . . 13 ⊢ (a ∈ (m +c 1c) ↔ ∃b ∈ m ∃x ∈ ∼ ba = (b ∪ {x}))
98		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ x ∈ V
99	98	elcompl 3226	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ ∼ b ↔ ¬ x ∈ b)
100	99	anbi2i 675	. . . . . . . . . . . . . . 15 ⊢ ((b ∈ m ∧ x ∈ ∼ b) ↔ (b ∈ m ∧ ¬ x ∈ b))
101		simp1r 980	. . . . . . . . . . . . . . . . . . 19 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → n ∈ Nn )
102		nnc0suc 4413	. . . . . . . . . . . . . . . . . . 19 ⊢ (n ∈ Nn ↔ (n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)))
103	101, 102	sylib 188	. . . . . . . . . . . . . . . . . 18 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → (n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)))
104		ssun2 3428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {x} ⊆ (b ∪ {x})
105	98	snid 3761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ x ∈ {x}
106	104, 105	sselii 3271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ x ∈ (b ∪ {x})
107		n0i 3556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ∈ (b ∪ {x}) → ¬ (b ∪ {x}) = ∅)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ (b ∪ {x}) = ∅
109	45	eleq2i 2417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((b ∪ {x}) ∈ 0c ↔ (b ∪ {x}) ∈ {∅})
110		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ b ∈ V
111		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {x} ∈ V
112	110, 111	unex 4107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b ∪ {x}) ∈ V
113	112	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((b ∪ {x}) ∈ {∅} ↔ (b ∪ {x}) = ∅)
114	109, 113	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((b ∪ {x}) ∈ 0c ↔ (b ∪ {x}) = ∅)
115	108, 114	mtbir 290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ (b ∪ {x}) ∈ 0c
116		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n = 0c → ((b ∪ {x}) ∈ n ↔ (b ∪ {x}) ∈ 0c))
117	116	biimpcd 215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((b ∪ {x}) ∈ n → (n = 0c → (b ∪ {x}) ∈ 0c))
118	115, 117	mtoi 169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((b ∪ {x}) ∈ n → ¬ n = 0c)
119	118	adantl 452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → ¬ n = 0c)
120		orel1 371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ n = 0c → ((n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)) → ∃p ∈ Nn n = (p +c 1c)))
121	119, 120	syl 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → ((n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)) → ∃p ∈ Nn n = (p +c 1c)))
122		simpll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) ∧ (b ∪ {x}) ∈ (p +c 1c)) → p ∈ Nn )
123		simpr3r 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) → ¬ x ∈ b)
124	123	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) ∧ (b ∪ {x}) ∈ (p +c 1c)) → ¬ x ∈ b)
125		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) ∧ (b ∪ {x}) ∈ (p +c 1c)) → (b ∪ {x}) ∈ (p +c 1c))
126	110, 98	nnsucelr 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((p ∈ Nn ∧ (¬ x ∈ b ∧ (b ∪ {x}) ∈ (p +c 1c))) → b ∈ p)
127	122, 124, 125, 126	syl12anc 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) ∧ (b ∪ {x}) ∈ (p +c 1c)) → b ∈ p)
128	127	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) → ((b ∪ {x}) ∈ (p +c 1c) → b ∈ p))
129		ineq2 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (q = p → (m ∩ q) = (m ∩ p))
130	129	eqeq1d 2361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (q = p → ((m ∩ q) = ∅ ↔ (m ∩ p) = ∅))
131		equequ2 1686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (q = p → (m = q ↔ m = p))
132	130, 131	orbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (q = p → (((m ∩ q) = ∅ ∨ m = q) ↔ ((m ∩ p) = ∅ ∨ m = p)))
133	132	rspccv 2953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → (p ∈ Nn → ((m ∩ p) = ∅ ∨ m = p)))
134		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (b ∈ (m ∩ p) ↔ (b ∈ m ∧ b ∈ p))
135		n0i 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (b ∈ (m ∩ p) → ¬ (m ∩ p) = ∅)
136	134, 135	sylbir 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((b ∈ m ∧ b ∈ p) → ¬ (m ∩ p) = ∅)
137		pm2.53 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((m ∩ p) = ∅ ∨ m = p) → (¬ (m ∩ p) = ∅ → m = p))
138	136, 137	syl5 28	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((m ∩ p) = ∅ ∨ m = p) → ((b ∈ m ∧ b ∈ p) → m = p))
139	138	exp3a 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((m ∩ p) = ∅ ∨ m = p) → (b ∈ m → (b ∈ p → m = p)))
140	133, 139	syl6 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → (p ∈ Nn → (b ∈ m → (b ∈ p → m = p))))
141	140	com23 72	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → (b ∈ m → (p ∈ Nn → (b ∈ p → m = p))))
142	141	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ b ∈ m) → (p ∈ Nn → (b ∈ p → m = p)))
143	142	adantrr 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → (p ∈ Nn → (b ∈ p → m = p)))
144	143	3adant1 973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → (p ∈ Nn → (b ∈ p → m = p)))
145	144	impcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) → (b ∈ p → m = p))
146	128, 145	syld 40	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((p ∈ Nn ∧ ((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b))) → ((b ∪ {x}) ∈ (p +c 1c) → m = p))
147	146	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (p ∈ Nn → (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → ((b ∪ {x}) ∈ (p +c 1c) → m = p)))
148	147	com3l 75	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → ((b ∪ {x}) ∈ (p +c 1c) → (p ∈ Nn → m = p)))
149	148	imp 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ (p +c 1c)) → (p ∈ Nn → m = p))
150		addceq1 4384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (m = p → (m +c 1c) = (p +c 1c))
151	149, 150	syl6 29	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ (p +c 1c)) → (p ∈ Nn → (m +c 1c) = (p +c 1c)))
152		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (n = (p +c 1c) → ((b ∪ {x}) ∈ n ↔ (b ∪ {x}) ∈ (p +c 1c)))
153	152	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n = (p +c 1c) → ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) ↔ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ (p +c 1c))))
154		eqeq2 2362	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (n = (p +c 1c) → ((m +c 1c) = n ↔ (m +c 1c) = (p +c 1c)))
155	154	imbi2d 307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n = (p +c 1c) → ((p ∈ Nn → (m +c 1c) = n) ↔ (p ∈ Nn → (m +c 1c) = (p +c 1c))))
156	153, 155	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = (p +c 1c) → (((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → (p ∈ Nn → (m +c 1c) = n)) ↔ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ (p +c 1c)) → (p ∈ Nn → (m +c 1c) = (p +c 1c)))))
157	151, 156	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = (p +c 1c) → ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → (p ∈ Nn → (m +c 1c) = n)))
158	157	com3l 75	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → (p ∈ Nn → (n = (p +c 1c) → (m +c 1c) = n)))
159	158	rexlimdv 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → (∃p ∈ Nn n = (p +c 1c) → (m +c 1c) = n))
160	121, 159	syld 40	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) ∧ (b ∪ {x}) ∈ n) → ((n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)) → (m +c 1c) = n))
161	160	ex 423	. . . . . . . . . . . . . . . . . 18 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → ((b ∪ {x}) ∈ n → ((n = 0c ∨ ∃p ∈ Nn n = (p +c 1c)) → (m +c 1c) = n)))
162	103, 161	mpid 37	. . . . . . . . . . . . . . . . 17 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) ∧ (b ∈ m ∧ ¬ x ∈ b)) → ((b ∪ {x}) ∈ n → (m +c 1c) = n))
163	162	3expa 1151	. . . . . . . . . . . . . . . 16 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) ∧ (b ∈ m ∧ ¬ x ∈ b)) → ((b ∪ {x}) ∈ n → (m +c 1c) = n))
164		eleq1 2413	. . . . . . . . . . . . . . . . 17 ⊢ (a = (b ∪ {x}) → (a ∈ n ↔ (b ∪ {x}) ∈ n))
165	164	imbi1d 308	. . . . . . . . . . . . . . . 16 ⊢ (a = (b ∪ {x}) → ((a ∈ n → (m +c 1c) = n) ↔ ((b ∪ {x}) ∈ n → (m +c 1c) = n)))
166	163, 165	syl5ibrcom 213	. . . . . . . . . . . . . . 15 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) ∧ (b ∈ m ∧ ¬ x ∈ b)) → (a = (b ∪ {x}) → (a ∈ n → (m +c 1c) = n)))
167	100, 166	sylan2b 461	. . . . . . . . . . . . . 14 ⊢ ((((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) ∧ (b ∈ m ∧ x ∈ ∼ b)) → (a = (b ∪ {x}) → (a ∈ n → (m +c 1c) = n)))
168	167	rexlimdvva 2746	. . . . . . . . . . . . 13 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (∃b ∈ m ∃x ∈ ∼ ba = (b ∪ {x}) → (a ∈ n → (m +c 1c) = n)))
169	97, 168	syl5bi 208	. . . . . . . . . . . 12 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (a ∈ (m +c 1c) → (a ∈ n → (m +c 1c) = n)))
170	169	imp3a 420	. . . . . . . . . . 11 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → ((a ∈ (m +c 1c) ∧ a ∈ n) → (m +c 1c) = n))
171	96, 170	syl5bi 208	. . . . . . . . . 10 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (a ∈ ((m +c 1c) ∩ n) → (m +c 1c) = n))
172	171	exlimdv 1636	. . . . . . . . 9 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (∃a a ∈ ((m +c 1c) ∩ n) → (m +c 1c) = n))
173	95, 172	syl5bi 208	. . . . . . . 8 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (¬ ((m +c 1c) ∩ n) = ∅ → (m +c 1c) = n))
174	173	orrd 367	. . . . . . 7 ⊢ (((m ∈ Nn ∧ n ∈ Nn ) ∧ ∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q)) → (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n))
175	174	exp31 587	. . . . . 6 ⊢ (m ∈ Nn → (n ∈ Nn → (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n))))
176	175	com23 72	. . . . 5 ⊢ (m ∈ Nn → (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → (n ∈ Nn → (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n))))
177	176	ralrimdv 2704	. . . 4 ⊢ (m ∈ Nn → (∀q ∈ Nn ((m ∩ q) = ∅ ∨ m = q) → ∀n ∈ Nn (((m +c 1c) ∩ n) = ∅ ∨ (m +c 1c) = n)))
178	44, 59, 70, 75, 80, 94, 177	finds 4412	. . 3 ⊢ (M ∈ Nn → ∀n ∈ Nn ((M ∩ n) = ∅ ∨ M = n))
179		ineq2 3452	. . . . . 6 ⊢ (n = N → (M ∩ n) = (M ∩ N))
180	179	eqeq1d 2361	. . . . 5 ⊢ (n = N → ((M ∩ n) = ∅ ↔ (M ∩ N) = ∅))
181		eqeq2 2362	. . . . 5 ⊢ (n = N → (M = n ↔ M = N))
182	180, 181	orbi12d 690	. . . 4 ⊢ (n = N → (((M ∩ n) = ∅ ∨ M = n) ↔ ((M ∩ N) = ∅ ∨ M = N)))
183	182	rspccv 2953	. . 3 ⊢ (∀n ∈ Nn ((M ∩ n) = ∅ ∨ M = n) → (N ∈ Nn → ((M ∩ N) = ∅ ∨ M = N)))
184	178, 183	syl 15	. 2 ⊢ (M ∈ Nn → (N ∈ Nn → ((M ∩ N) = ∅ ∨ M = N)))
185	184	imp 418	1 ⊢ ((M ∈ Nn ∧ N ∈ Nn ) → ((M ∩ N) = ∅ ∨ M = N))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2517  ∀wral 2615  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∪ cun 3208   ∩ cin 3209  ∅c0 3551  {csn 3738  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136   Ins2_k cins2k 4177   Ins3_k cins3k 4178   “_k cimak 4180   S_k cssetk 4184   I_k cidk 4185   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-0c 4378  df-addc 4379  df-nnc 4380

This theorem is referenced by:  nnceleq  4431  sfinltfin  4536