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

Theorem phplem2 6713
 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 4119 . . . . . . 7
43snex 4077 . . . . . 6
51, 2f1osn 5373 . . . . . 6
6 f1oen3g 6614 . . . . . 6
74, 5, 6mp2an 420 . . . . 5
8 difss 3170 . . . . . . 7
92, 8ssexi 4034 . . . . . 6
109enref 6625 . . . . 5
117, 10pm3.2i 268 . . . 4
12 incom 3236 . . . . . 6
13 ssrin 3269 . . . . . . . . 9
148, 13ax-mp 5 . . . . . . . 8
15 nnord 4493 . . . . . . . . 9
16 orddisj 4429 . . . . . . . . 9
1715, 16syl 14 . . . . . . . 8
1814, 17sseqtrid 3115 . . . . . . 7
19 ss0 3371 . . . . . . 7
2018, 19syl 14 . . . . . 6
2112, 20syl5eq 2160 . . . . 5
22 disjdif 3403 . . . . 5
2321, 22jctil 308 . . . 4
24 unen 6676 . . . 4
2511, 23, 24sylancr 408 . . 3