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

Theorem onintonm 4269
 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 2994 . . . . . . 7
2 eloni 4138 . . . . . . . 8
3 ordtr 4141 . . . . . . . 8
42, 3syl 14 . . . . . . 7
51, 4syl6 33 . . . . . 6
65ralrimiv 2434 . . . . 5
7 trint 3898 . . . . 5
86, 7syl 14 . . . 4
10 nfv 1462 . . . . 5
11 nfe1 1426 . . . . 5
1210, 11nfan 1498 . . . 4
13 intssuni2m 3668 . . . . . . . 8
14 unon 4263 . . . . . . . 8
1513, 14syl6sseq 3046 . . . . . . 7
1615sseld 2999 . . . . . 6
1716, 2syl6 33 . . . . 5
1817, 3syl6 33 . . . 4
1912, 18ralrimi 2433 . . 3
20 dford3 4130 . . 3
219, 19, 20sylanbrc 408 . 2
22 inteximm 3932 . . . 4