NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nndisjeq GIF version

Theorem nndisjeq 4429
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 ) → ((MN) = M = N))

Proof of Theorem nndisjeq
Dummy variables a b m n q x p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . . 8 p V
21elcompl 3225 . . . . . . 7 (p ∼ ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) ↔ ¬ p ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ))
31elimak 4259 . . . . . . . . 9 (p ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) ↔ n Nnn, p ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ))
4 opkex 4113 . . . . . . . . . . . 12 n, p V
54elcompl 3225 . . . . . . . . . . 11 (⟪n, p ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) ↔ ¬ ⟪n, p ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ))
6 elun 3220 . . . . . . . . . . . 12 (⟪n, p ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) ↔ (⟪n, p ∼ (( Ins3k SkIns2k Sk ) “k 111c) n, p Ik ))
7 vex 2862 . . . . . . . . . . . . . . . 16 n V
87, 1ndisjrelk 4323 . . . . . . . . . . . . . . 15 (⟪n, p (( Ins3k SkIns2k Sk ) “k 111c) ↔ (np) ≠ )
98notbii 287 . . . . . . . . . . . . . 14 (¬ ⟪n, p (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (np) ≠ )
104elcompl 3225 . . . . . . . . . . . . . 14 (⟪n, p ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪n, p (( Ins3k SkIns2k Sk ) “k 111c))
11 df-ne 2518 . . . . . . . . . . . . . . 15 ((np) ≠ ↔ ¬ (np) = )
1211con2bii 322 . . . . . . . . . . . . . 14 ((np) = ↔ ¬ (np) ≠ )
139, 10, 123bitr4i 268 . . . . . . . . . . . . 13 (⟪n, p ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (np) = )
14 opkelidkg 4274 . . . . . . . . . . . . . 14 ((n V p V) → (⟪n, p Ikn = p))
157, 1, 14mp2an 653 . . . . . . . . . . . . 13 (⟪n, p Ikn = p)
1613, 15orbi12i 507 . . . . . . . . . . . 12 ((⟪n, p ∼ (( Ins3k SkIns2k Sk ) “k 111c) n, p Ik ) ↔ ((np) = n = p))
17 incom 3448 . . . . . . . . . . . . . 14 (np) = (pn)
1817eqeq1i 2360 . . . . . . . . . . . . 13 ((np) = ↔ (pn) = )
19 eqcom 2355 . . . . . . . . . . . . 13 (n = pp = n)
2018, 19orbi12i 507 . . . . . . . . . . . 12 (((np) = n = p) ↔ ((pn) = p = n))
216, 16, 203bitri 262 . . . . . . . . . . 11 (⟪n, p ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) ↔ ((pn) = p = n))
225, 21xchbinx 301 . . . . . . . . . 10 (⟪n, p ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) ↔ ¬ ((pn) = p = n))
2322rexbii 2639 . . . . . . . . 9 (n Nnn, p ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) ↔ n Nn ¬ ((pn) = p = n))
24 rexnal 2625 . . . . . . . . 9 (n Nn ¬ ((pn) = p = n) ↔ ¬ n Nn ((pn) = p = n))
253, 23, 243bitri 262 . . . . . . . 8 (p ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) ↔ ¬ n Nn ((pn) = p = n))
2625con2bii 322 . . . . . . 7 (n Nn ((pn) = p = n) ↔ ¬ p ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ))
272, 26bitr4i 243 . . . . . 6 (p ∼ ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) ↔ n Nn ((pn) = p = n))
2827abbi2i 2464 . . . . 5 ∼ ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) = {p n Nn ((pn) = p = n)}
29 ssetkex 4294 . . . . . . . . . . . . 13 Sk V
3029ins3kex 4308 . . . . . . . . . . . 12 Ins3k Sk V
3129ins2kex 4307 . . . . . . . . . . . 12 Ins2k Sk V
3230, 31inex 4105 . . . . . . . . . . 11 ( Ins3k SkIns2k Sk ) V
33 1cex 4142 . . . . . . . . . . . . 13 1c V
3433pw1ex 4303 . . . . . . . . . . . 12 11c V
3534pw1ex 4303 . . . . . . . . . . 11 111c V
3632, 35imakex 4300 . . . . . . . . . 10 (( Ins3k SkIns2k Sk ) “k 111c) V
3736complex 4104 . . . . . . . . 9 ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
38 idkex 4314 . . . . . . . . 9 Ik V
3937, 38unex 4106 . . . . . . . 8 ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) V
4039complex 4104 . . . . . . 7 ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) V
41 nncex 4396 . . . . . . 7 Nn V
4240, 41imakex 4300 . . . . . 6 ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) V
4342complex 4104 . . . . 5 ∼ ( ∼ ( ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∪ Ik ) “k Nn ) V
4428, 43eqeltrri 2424 . . . 4 {p n Nn ((pn) = p = n)} V
45 df-0c 4377 . . . . . . . . . . 11 0c = {}
4645eqeq2i 2363 . . . . . . . . . 10 (p = 0cp = {})
4746biimpi 186 . . . . . . . . 9 (p = 0cp = {})
4847ineq1d 3456 . . . . . . . 8 (p = 0c → (pn) = ({} ∩ n))
4948eqeq1d 2361 . . . . . . 7 (p = 0c → ((pn) = ↔ ({} ∩ n) = ))
50 incom 3448 . . . . . . . . 9 ({} ∩ n) = (n ∩ {})
5150eqeq1i 2360 . . . . . . . 8 (({} ∩ n) = ↔ (n ∩ {}) = )
52 disjsn 3786 . . . . . . . 8 ((n ∩ {}) = ↔ ¬ n)
5351, 52bitri 240 . . . . . . 7 (({} ∩ n) = ↔ ¬ n)
5449, 53syl6bb 252 . . . . . 6 (p = 0c → ((pn) = ↔ ¬ n))
55 eqeq1 2359 . . . . . . 7 (p = 0c → (p = n ↔ 0c = n))
56 eqcom 2355 . . . . . . 7 (0c = nn = 0c)
5755, 56syl6bb 252 . . . . . 6 (p = 0c → (p = nn = 0c))
5854, 57orbi12d 690 . . . . 5 (p = 0c → (((pn) = p = n) ↔ (¬ n n = 0c)))
5958ralbidv 2634 . . . 4 (p = 0c → (n Nn ((pn) = p = n) ↔ n Nn n n = 0c)))
60 ineq1 3450 . . . . . . . 8 (p = m → (pn) = (mn))
6160eqeq1d 2361 . . . . . . 7 (p = m → ((pn) = ↔ (mn) = ))
62 eqeq1 2359 . . . . . . 7 (p = m → (p = nm = n))
6361, 62orbi12d 690 . . . . . 6 (p = m → (((pn) = p = n) ↔ ((mn) = m = n)))
6463ralbidv 2634 . . . . 5 (p = m → (n Nn ((pn) = p = n) ↔ n Nn ((mn) = m = n)))
65 ineq2 3451 . . . . . . . 8 (n = q → (mn) = (mq))
6665eqeq1d 2361 . . . . . . 7 (n = q → ((mn) = ↔ (mq) = ))
67 equequ2 1686 . . . . . . 7 (n = q → (m = nm = q))
6866, 67orbi12d 690 . . . . . 6 (n = q → (((mn) = m = n) ↔ ((mq) = m = q)))
6968cbvralv 2835 . . . . 5 (n Nn ((mn) = m = n) ↔ q Nn ((mq) = m = q))
7064, 69syl6bb 252 . . . 4 (p = m → (n Nn ((pn) = p = n) ↔ q Nn ((mq) = m = q)))
71 ineq1 3450 . . . . . . 7 (p = (m +c 1c) → (pn) = ((m +c 1c) ∩ n))
7271eqeq1d 2361 . . . . . 6 (p = (m +c 1c) → ((pn) = ↔ ((m +c 1c) ∩ n) = ))
73 eqeq1 2359 . . . . . 6 (p = (m +c 1c) → (p = n ↔ (m +c 1c) = n))
7472, 73orbi12d 690 . . . . 5 (p = (m +c 1c) → (((pn) = p = n) ↔ (((m +c 1c) ∩ n) = (m +c 1c) = n)))
7574ralbidv 2634 . . . 4 (p = (m +c 1c) → (n Nn ((pn) = p = n) ↔ n Nn (((m +c 1c) ∩ n) = (m +c 1c) = n)))
76 ineq1 3450 . . . . . . 7 (p = M → (pn) = (Mn))
7776eqeq1d 2361 . . . . . 6 (p = M → ((pn) = ↔ (Mn) = ))
78 eqeq1 2359 . . . . . 6 (p = M → (p = nM = n))
7977, 78orbi12d 690 . . . . 5 (p = M → (((pn) = p = n) ↔ ((Mn) = M = n)))
8079ralbidv 2634 . . . 4 (p = M → (n Nn ((pn) = p = n) ↔ n Nn ((Mn) = M = n)))
81 nnc0suc 4412 . . . . . . 7 (n Nn ↔ (n = 0c m Nn n = (m +c 1c)))
82 0nelsuc 4400 . . . . . . . . . . . 12 ¬ (m +c 1c)
83 eleq2 2414 . . . . . . . . . . . . 13 (n = (m +c 1c) → ( n (m +c 1c)))
8483biimpcd 215 . . . . . . . . . . . 12 ( n → (n = (m +c 1c) → (m +c 1c)))
8582, 84mtoi 169 . . . . . . . . . . 11 ( n → ¬ n = (m +c 1c))
8685adantr 451 . . . . . . . . . 10 (( n m Nn ) → ¬ n = (m +c 1c))
8786nrexdv 2717 . . . . . . . . 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))
8987, 88syl 15 . . . . . . . 8 ( n → ((n = 0c m Nn n = (m +c 1c)) → n = 0c))
9089com12 27 . . . . . . 7 ((n = 0c m Nn n = (m +c 1c)) → ( nn = 0c))
9181, 90sylbi 187 . . . . . 6 (n Nn → ( nn = 0c))
92 imor 401 . . . . . 6 (( nn = 0c) ↔ (¬ n n = 0c))
9391, 92sylib 188 . . . . 5 (n Nn → (¬ n n = 0c))
9493rgen 2679 . . . 4 n Nn n n = 0c)
95 neq0 3560 . . . . . . . . 9 (¬ ((m +c 1c) ∩ n) = a a ((m +c 1c) ∩ n))
96 elin 3219 . . . . . . . . . . 11 (a ((m +c 1c) ∩ n) ↔ (a (m +c 1c) a n))
97 elsuc 4413 . . . . . . . . . . . . 13 (a (m +c 1c) ↔ b m x ba = (b ∪ {x}))
98 vex 2862 . . . . . . . . . . . . . . . . 17 x V
9998elcompl 3225 . . . . . . . . . . . . . . . 16 (x b ↔ ¬ x b)
10099anbi2i 675 . . . . . . . . . . . . . . 15 ((b m x b) ↔ (b m ¬ x b))
101 simp1r 980 . . . . . . . . . . . . . . . . . . 19 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → n Nn )
102 nnc0suc 4412 . . . . . . . . . . . . . . . . . . 19 (n Nn ↔ (n = 0c p Nn n = (p +c 1c)))
103101, 102sylib 188 . . . . . . . . . . . . . . . . . 18 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → (n = 0c p Nn n = (p +c 1c)))
104 ssun2 3427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {x} (b ∪ {x})
10598snid 3760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 x {x}
106104, 105sselii 3270 . . . . . . . . . . . . . . . . . . . . . . . . 25 x (b ∪ {x})
107 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x (b ∪ {x}) → ¬ (b ∪ {x}) = )
108106, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ (b ∪ {x}) =
10945eleq2i 2417 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b ∪ {x}) 0c ↔ (b ∪ {x}) {})
110 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 b V
111 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {x} V
112110, 111unex 4106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b ∪ {x}) V
113112elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b ∪ {x}) {} ↔ (b ∪ {x}) = )
114109, 113bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 ((b ∪ {x}) 0c ↔ (b ∪ {x}) = )
115108, 114mtbir 290 . . . . . . . . . . . . . . . . . . . . . . 23 ¬ (b ∪ {x}) 0c
116 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . 24 (n = 0c → ((b ∪ {x}) n ↔ (b ∪ {x}) 0c))
117116biimpcd 215 . . . . . . . . . . . . . . . . . . . . . . 23 ((b ∪ {x}) n → (n = 0c → (b ∪ {x}) 0c))
118115, 117mtoi 169 . . . . . . . . . . . . . . . . . . . . . 22 ((b ∪ {x}) n → ¬ n = 0c)
119118adantl 452 . . . . . . . . . . . . . . . . . . . . 21 ((((m Nn n Nn ) q Nn ((mq) = 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)))
121119, 120syl 15 . . . . . . . . . . . . . . . . . . . 20 ((((m Nn n Nn ) q Nn ((mq) = 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 ((mq) = 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 ((mq) = m = q) (b m ¬ x b))) → ¬ x b)
124123adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((p Nn ((m Nn n Nn ) q Nn ((mq) = 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 ((mq) = m = q) (b m ¬ x b))) (b ∪ {x}) (p +c 1c)) → (b ∪ {x}) (p +c 1c))
126110, 98nnsucelr 4428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((p Nn x b (b ∪ {x}) (p +c 1c))) → b p)
127122, 124, 125, 126syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((p Nn ((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b))) (b ∪ {x}) (p +c 1c)) → b p)
128127ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((p Nn ((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b))) → ((b ∪ {x}) (p +c 1c) → b p))
129 ineq2 3451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (q = p → (mq) = (mp))
130129eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (q = p → ((mq) = ↔ (mp) = ))
131 equequ2 1686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (q = p → (m = qm = p))
132130, 131orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (q = p → (((mq) = m = q) ↔ ((mp) = m = p)))
133132rspccv 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (q Nn ((mq) = m = q) → (p Nn → ((mp) = m = p)))
134 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (b (mp) ↔ (b m b p))
135 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (b (mp) → ¬ (mp) = )
136134, 135sylbir 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((b m b p) → ¬ (mp) = )
137 pm2.53 362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((mp) = m = p) → (¬ (mp) = m = p))
138136, 137syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((mp) = m = p) → ((b m b p) → m = p))
139138exp3a 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((mp) = m = p) → (b m → (b pm = p)))
140133, 139syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (q Nn ((mq) = m = q) → (p Nn → (b m → (b pm = p))))
141140com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (q Nn ((mq) = m = q) → (b m → (p Nn → (b pm = p))))
142141imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((q Nn ((mq) = m = q) b m) → (p Nn → (b pm = p)))
143142adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((q Nn ((mq) = m = q) (b m ¬ x b)) → (p Nn → (b pm = p)))
1441433adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → (p Nn → (b pm = p)))
145144impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((p Nn ((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b))) → (b pm = p))
146128, 145syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((p Nn ((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b))) → ((b ∪ {x}) (p +c 1c) → m = p))
147146ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (p Nn → (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → ((b ∪ {x}) (p +c 1c) → m = p)))
148147com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → ((b ∪ {x}) (p +c 1c) → (p Nnm = p)))
149148imp 418 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) (p +c 1c)) → (p Nnm = p))
150 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = p → (m +c 1c) = (p +c 1c))
151149, 150syl6 29 . . . . . . . . . . . . . . . . . . . . . . 23 ((((m Nn n Nn ) q Nn ((mq) = 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)))
153152anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . 24 (n = (p +c 1c) → ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) ↔ (((m Nn n Nn ) q Nn ((mq) = 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)))
155154imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . 24 (n = (p +c 1c) → ((p Nn → (m +c 1c) = n) ↔ (p Nn → (m +c 1c) = (p +c 1c))))
156153, 155imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . 23 (n = (p +c 1c) → (((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) → (p Nn → (m +c 1c) = n)) ↔ ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) (p +c 1c)) → (p Nn → (m +c 1c) = (p +c 1c)))))
157151, 156mpbiri 224 . . . . . . . . . . . . . . . . . . . . . 22 (n = (p +c 1c) → ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) → (p Nn → (m +c 1c) = n)))
158157com3l 75 . . . . . . . . . . . . . . . . . . . . 21 ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) → (p Nn → (n = (p +c 1c) → (m +c 1c) = n)))
159158rexlimdv 2737 . . . . . . . . . . . . . . . . . . . 20 ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) → (p Nn n = (p +c 1c) → (m +c 1c) = n))
160121, 159syld 40 . . . . . . . . . . . . . . . . . . 19 ((((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) (b ∪ {x}) n) → ((n = 0c p Nn n = (p +c 1c)) → (m +c 1c) = n))
161160ex 423 . . . . . . . . . . . . . . . . . 18 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → ((b ∪ {x}) n → ((n = 0c p Nn n = (p +c 1c)) → (m +c 1c) = n)))
162103, 161mpid 37 . . . . . . . . . . . . . . . . 17 (((m Nn n Nn ) q Nn ((mq) = m = q) (b m ¬ x b)) → ((b ∪ {x}) n → (m +c 1c) = n))
1631623expa 1151 . . . . . . . . . . . . . . . 16 ((((m Nn n Nn ) q Nn ((mq) = 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))
165164imbi1d 308 . . . . . . . . . . . . . . . 16 (a = (b ∪ {x}) → ((a n → (m +c 1c) = n) ↔ ((b ∪ {x}) n → (m +c 1c) = n)))
166163, 165syl5ibrcom 213 . . . . . . . . . . . . . . 15 ((((m Nn n Nn ) q Nn ((mq) = m = q)) (b m ¬ x b)) → (a = (b ∪ {x}) → (a n → (m +c 1c) = n)))
167100, 166sylan2b 461 . . . . . . . . . . . . . 14 ((((m Nn n Nn ) q Nn ((mq) = m = q)) (b m x b)) → (a = (b ∪ {x}) → (a n → (m +c 1c) = n)))
168167rexlimdvva 2745 . . . . . . . . . . . . 13 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (b m x ba = (b ∪ {x}) → (a n → (m +c 1c) = n)))
16997, 168syl5bi 208 . . . . . . . . . . . 12 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (a (m +c 1c) → (a n → (m +c 1c) = n)))
170169imp3a 420 . . . . . . . . . . 11 (((m Nn n Nn ) q Nn ((mq) = m = q)) → ((a (m +c 1c) a n) → (m +c 1c) = n))
17196, 170syl5bi 208 . . . . . . . . . 10 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (a ((m +c 1c) ∩ n) → (m +c 1c) = n))
172171exlimdv 1636 . . . . . . . . 9 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (a a ((m +c 1c) ∩ n) → (m +c 1c) = n))
17395, 172syl5bi 208 . . . . . . . 8 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (¬ ((m +c 1c) ∩ n) = → (m +c 1c) = n))
174173orrd 367 . . . . . . 7 (((m Nn n Nn ) q Nn ((mq) = m = q)) → (((m +c 1c) ∩ n) = (m +c 1c) = n))
175174exp31 587 . . . . . 6 (m Nn → (n Nn → (q Nn ((mq) = m = q) → (((m +c 1c) ∩ n) = (m +c 1c) = n))))
176175com23 72 . . . . 5 (m Nn → (q Nn ((mq) = m = q) → (n Nn → (((m +c 1c) ∩ n) = (m +c 1c) = n))))
177176ralrimdv 2703 . . . 4 (m Nn → (q Nn ((mq) = m = q) → n Nn (((m +c 1c) ∩ n) = (m +c 1c) = n)))
17844, 59, 70, 75, 80, 94, 177finds 4411 . . 3 (M Nnn Nn ((Mn) = M = n))
179 ineq2 3451 . . . . . 6 (n = N → (Mn) = (MN))
180179eqeq1d 2361 . . . . 5 (n = N → ((Mn) = ↔ (MN) = ))
181 eqeq2 2362 . . . . 5 (n = N → (M = nM = N))
182180, 181orbi12d 690 . . . 4 (n = N → (((Mn) = M = n) ↔ ((MN) = M = N)))
183182rspccv 2952 . . 3 (n Nn ((Mn) = M = n) → (N Nn → ((MN) = M = N)))
184178, 183syl 15 . 2 (M Nn → (N Nn → ((MN) = M = N)))
185184imp 418 1 ((M Nn N Nn ) → ((MN) = M = N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358   w3a 934  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wral 2614  wrex 2615  Vcvv 2859  ccompl 3205  cun 3207  cin 3208  c0 3550  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   Sk cssetk 4183   Ik cidk 4184   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379
This theorem is referenced by:  nnceleq  4430  sfinltfin  4535
  Copyright terms: Public domain W3C validator