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

Metamath Proof Explorer

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 ) ) = (/)