Metamath Proof Explorer


Theorem iinon

Description: The nonempty indexed intersection of a class of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion iinon x A B On A x A B On

Proof

Step Hyp Ref Expression
1 dfiin3g x A B On x A B = ran x A B
2 1 adantr x A B On A x A B = ran x A B
3 eqid x A B = x A B
4 3 rnmptss x A B On ran x A B On
5 dm0rn0 dom x A B = ran x A B =
6 dmmptg x A B On dom x A B = A
7 6 eqeq1d x A B On dom x A B = A =
8 5 7 bitr3id x A B On ran x A B = A =
9 8 necon3bid x A B On ran x A B A
10 9 biimpar x A B On A ran x A B
11 oninton ran x A B On ran x A B ran x A B On
12 4 10 11 syl2an2r x A B On A ran x A B On
13 2 12 eqeltrd x A B On A x A B On