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 )