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

Theorem onintonm 4442
 Description: The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)
Assertion
Ref Expression
onintonm
Distinct variable group:   ,

Proof of Theorem onintonm
StepHypRef Expression
1 ssel 3097 . . . . . . 7
2 eloni 4306 . . . . . . . 8
3 ordtr 4309 . . . . . . . 8
42, 3syl 14 . . . . . . 7
51, 4syl6 33 . . . . . 6
65ralrimiv 2508 . . . . 5
7 trint 4050 . . . . 5
86, 7syl 14 . . . 4
10 nfv 1509 . . . . 5
11 nfe1 1473 . . . . 5
1210, 11nfan 1545 . . . 4
13 intssuni2m 3804 . . . . . . . 8
14 unon 4436 . . . . . . . 8
1513, 14sseqtrdi 3151 . . . . . . 7
1615sseld 3102 . . . . . 6
1716, 2syl6 33 . . . . 5
1817, 3syl6 33 . . . 4
1912, 18ralrimi 2507 . . 3
20 dford3 4298 . . 3
219, 19, 20sylanbrc 414 . 2
22 inteximm 4083 . . . 4