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

Theorem onsucuni2 4474
 Description: A successor ordinal is the successor of its union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
onsucuni2

Proof of Theorem onsucuni2
StepHypRef Expression
1 eleq1 2200 . . . . . 6
21biimpac 296 . . . . 5
3 sucelon 4414 . . . . . . 7
4 eloni 4292 . . . . . . . . . 10
5 ordtr 4295 . . . . . . . . . 10
64, 5syl 14 . . . . . . . . 9
7 unisucg 4331 . . . . . . . . 9
86, 7mpbid 146 . . . . . . . 8
9 suceq 4319 . . . . . . . 8
108, 9syl 14 . . . . . . 7
113, 10sylbir 134 . . . . . 6
12 eloni 4292 . . . . . . . 8
13 ordtr 4295 . . . . . . . 8
1412, 13syl 14 . . . . . . 7
15 unisucg 4331 . . . . . . 7
1614, 15mpbid 146 . . . . . 6
1711, 16eqtr4d 2173 . . . . 5
182, 17syl 14 . . . 4
19 unieq 3740 . . . . . 6
20 suceq 4319 . . . . . 6
2119, 20syl 14 . . . . 5
22 suceq 4319 . . . . . 6
2322unieqd 3742 . . . . 5
2421, 23eqeq12d 2152 . . . 4
2518, 24syl5ibr 155 . . 3
2625anabsi7 570 . 2
27 eloni 4292 . . . . 5
28 ordtr 4295 . . . . 5
2927, 28syl 14 . . . 4
30 unisucg 4331 . . . 4
3129, 30mpbid 146 . . 3