This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A. x e. A B e. On /\ A =/= (/) ) -> |^|_ x e. A B e. On )

Proof

Step Hyp Ref Expression
1 dfiin3g 
 |-  ( A. x e. A B e. On -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )
2 1 adantr 
 |-  ( ( A. x e. A B e. On /\ A =/= (/) ) -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )
3 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
4 3 rnmptss 
 |-  ( A. x e. A B e. On -> ran ( x e. A |-> B ) C_ On )
5 dm0rn0 
 |-  ( dom ( x e. A |-> B ) = (/) <-> ran ( x e. A |-> B ) = (/) )
6 dmmptg 
 |-  ( A. x e. A B e. On -> dom ( x e. A |-> B ) = A )
7 6 eqeq1d 
 |-  ( A. x e. A B e. On -> ( dom ( x e. A |-> B ) = (/) <-> A = (/) ) )
8 5 7 bitr3id 
 |-  ( A. x e. A B e. On -> ( ran ( x e. A |-> B ) = (/) <-> A = (/) ) )
9 8 necon3bid 
 |-  ( A. x e. A B e. On -> ( ran ( x e. A |-> B ) =/= (/) <-> A =/= (/) ) )
10 9 biimpar 
 |-  ( ( A. x e. A B e. On /\ A =/= (/) ) -> ran ( x e. A |-> B ) =/= (/) )
11 oninton 
 |-  ( ( ran ( x e. A |-> B ) C_ On /\ ran ( x e. A |-> B ) =/= (/) ) -> |^| ran ( x e. A |-> B ) e. On )
12 4 10 11 syl2an2r 
 |-  ( ( A. x e. A B e. On /\ A =/= (/) ) -> |^| ran ( x e. A |-> B ) e. On )
13 2 12 eqeltrd 
 |-  ( ( A. x e. A B e. On /\ A =/= (/) ) -> |^|_ x e. A B e. On )