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 ∩ V × V = ∅

Proof

Step Hyp Ref Expression
1 disj ⊢ On ∩ V × V = ∅ ↔ ∀ x ∈ On ¬ x ∈ V × V
2 on0eqel ⊢ x ∈ On → x = ∅ ∨ ∅ ∈ x
3 0nelxp ⊢ ¬ ∅ ∈ V × V
4 eleq1 ⊢ x = ∅ → x ∈ V × V ↔ ∅ ∈ V × V
5 3 4 mtbiri ⊢ x = ∅ → ¬ x ∈ V × V
6 0nelelxp ⊢ x ∈ V × V → ¬ ∅ ∈ x
7 6 con2i ⊢ ∅ ∈ x → ¬ x ∈ V × V
8 5 7 jaoi ⊢ x = ∅ ∨ ∅ ∈ x → ¬ x ∈ V × V
9 2 8 syl ⊢ x ∈ On → ¬ x ∈ V × V
10 1 9 mprgbir ⊢ On ∩ V × V = ∅