Description: Obsolete version of sdom0 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sdom0OLD | ⊢ ¬ 𝐴 ≺ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relsdom | ⊢ Rel ≺ | |
2 | 1 | brrelex1i | ⊢ ( 𝐴 ≺ ∅ → 𝐴 ∈ V ) |
3 | 0domg | ⊢ ( 𝐴 ∈ V → ∅ ≼ 𝐴 ) | |
4 | 2 3 | syl | ⊢ ( 𝐴 ≺ ∅ → ∅ ≼ 𝐴 ) |
5 | domnsym | ⊢ ( ∅ ≼ 𝐴 → ¬ 𝐴 ≺ ∅ ) | |
6 | 5 | con2i | ⊢ ( 𝐴 ≺ ∅ → ¬ ∅ ≼ 𝐴 ) |
7 | 4 6 | pm2.65i | ⊢ ¬ 𝐴 ≺ ∅ |