Theorem onxpdisj

Description: Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non . (Contributed by NM, 1-Jun-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	onxpdisj	|- ( On i^i ( _V X. _V ) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		disj	|- ( ( On i^i ( _V X. _V ) ) = (/) <-> A. x e. On -. x e. ( _V X. _V ) )
2		on0eqel	|- ( x e. On -> ( x = (/) \/ (/) e. x ) )
3		0nelxp	|- -. (/) e. ( _V X. _V )
4		eleq1	|- ( x = (/) -> ( x e. ( _V X. _V ) <-> (/) e. ( _V X. _V ) ) )
5	3 4	mtbiri	|- ( x = (/) -> -. x e. ( _V X. _V ) )
6		0nelelxp	|- ( x e. ( _V X. _V ) -> -. (/) e. x )
7	6	con2i	|- ( (/) e. x -> -. x e. ( _V X. _V ) )
8	5 7	jaoi	|- ( ( x = (/) \/ (/) e. x ) -> -. x e. ( _V X. _V ) )
9	2 8	syl	|- ( x e. On -> -. x e. ( _V X. _V ) )
10	1 9	mprgbir	|- ( On i^i ( _V X. _V ) ) = (/)