Theorem onint0

Description: The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	onint0	|- ( A C_ On -> ( |^| A = (/) <-> (/) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		eleq1	|- ( |^| A = (/) -> ( |^| A e. _V <-> (/) e. _V ) )
3	1 2	mpbiri	|- ( |^| A = (/) -> |^| A e. _V )
4		intex	|- ( A =/= (/) <-> |^| A e. _V )
5	3 4	sylibr	|- ( |^| A = (/) -> A =/= (/) )
6		onint	|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
7	5 6	sylan2	|- ( ( A C_ On /\ |^| A = (/) ) -> |^| A e. A )
8		eleq1	|- ( |^| A = (/) -> ( |^| A e. A <-> (/) e. A ) )
9	8	adantl	|- ( ( A C_ On /\ |^| A = (/) ) -> ( |^| A e. A <-> (/) e. A ) )
10	7 9	mpbid	|- ( ( A C_ On /\ |^| A = (/) ) -> (/) e. A )
11	10	ex	|- ( A C_ On -> ( |^| A = (/) -> (/) e. A ) )
12		int0el	|- ( (/) e. A -> |^| A = (/) )
13	11 12	impbid1	|- ( A C_ On -> ( |^| A = (/) <-> (/) e. A ) )