Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  phplem2 Unicode version

Theorem phplem2 6409
 Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.)
Hypotheses
Ref Expression
phplem2.1
phplem2.2
Assertion
Ref Expression
phplem2

Proof of Theorem phplem2
StepHypRef Expression
1 phplem2.2 . . . . . . . 8
2 phplem2.1 . . . . . . . 8
31, 2opex 4012 . . . . . . 7
43snex 3977 . . . . . 6
51, 2f1osn 5217 . . . . . 6
6 f1oen3g 6322 . . . . . 6
74, 5, 6mp2an 417 . . . . 5
8 difss 3108 . . . . . . 7
92, 8ssexi 3936 . . . . . 6
109enref 6333 . . . . 5
117, 10pm3.2i 266 . . . 4
12 incom 3174 . . . . . 6
13 ssrin 3207 . . . . . . . . 9
148, 13ax-mp 7 . . . . . . . 8
15 nnord 4380 . . . . . . . . 9
16 orddisj 4317 . . . . . . . . 9
1715, 16syl 14 . . . . . . . 8
1814, 17syl5sseq 3056 . . . . . . 7
19 ss0 3300 . . . . . . 7
2018, 19syl 14 . . . . . 6
2112, 20syl5eq 2127 . . . . 5
22 disjdif 3332 . . . . 5
2321, 22jctil 305 . . . 4
24 unen 6382 . . . 4
2511, 23, 24sylancr 405 . . 3