Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets (cont.)
1sdom2
Metamath Proof Explorer
Description: Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof
requiring ax-un , see 1sdom2ALT . (Contributed by NM , 4-Apr-2007)
Avoid ax-un . (Revised by BTernaryTau , 8-Dec-2024)
Ref
Expression
Assertion
1sdom2
⊢ 1 𝑜 ≺ 2 𝑜
Proof
Step
Hyp
Ref
Expression
1
2on0
⊢ 2 𝑜 ≠ ∅
2
2oex
⊢ 2 𝑜 ∈ V
3
2
0sdom
⊢ ∅ ≺ 2 𝑜 ↔ 2 𝑜 ≠ ∅
4
1 3
mpbir
⊢ ∅ ≺ 2 𝑜
5
0sdom1dom
⊢ ∅ ≺ 2 𝑜 ↔ 1 𝑜 ≼ 2 𝑜
6
4 5
mpbi
⊢ 1 𝑜 ≼ 2 𝑜
7
snnen2o
⊢ ¬ ∅ ≈ 2 𝑜
8
df1o2
⊢ 1 𝑜 = ∅
9
8
breq1i
⊢ 1 𝑜 ≈ 2 𝑜 ↔ ∅ ≈ 2 𝑜
10
7 9
mtbir
⊢ ¬ 1 𝑜 ≈ 2 𝑜
11
brsdom
⊢ 1 𝑜 ≺ 2 𝑜 ↔ 1 𝑜 ≼ 2 𝑜 ∧ ¬ 1 𝑜 ≈ 2 𝑜
12
6 10 11
mpbir2an
⊢ 1 𝑜 ≺ 2 𝑜