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 ) ) = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | disj | ⊢ ( ( On ∩ ( V × V ) ) = ∅ ↔ ∀ 𝑥 ∈ On ¬ 𝑥 ∈ ( V × V ) ) | |
| 2 | on0eqel | ⊢ ( 𝑥 ∈ On → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) ) | |
| 3 | 0nelxp | ⊢ ¬ ∅ ∈ ( V × V ) | |
| 4 | eleq1 | ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ ( V × V ) ↔ ∅ ∈ ( V × V ) ) ) | |
| 5 | 3 4 | mtbiri | ⊢ ( 𝑥 = ∅ → ¬ 𝑥 ∈ ( V × V ) ) |
| 6 | 0nelelxp | ⊢ ( 𝑥 ∈ ( V × V ) → ¬ ∅ ∈ 𝑥 ) | |
| 7 | 6 | con2i | ⊢ ( ∅ ∈ 𝑥 → ¬ 𝑥 ∈ ( V × V ) ) |
| 8 | 5 7 | jaoi | ⊢ ( ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) → ¬ 𝑥 ∈ ( V × V ) ) |
| 9 | 2 8 | syl | ⊢ ( 𝑥 ∈ On → ¬ 𝑥 ∈ ( V × V ) ) |
| 10 | 1 9 | mprgbir | ⊢ ( On ∩ ( V × V ) ) = ∅ |