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

Metamath Proof Explorer

Theorem 1sdom

Description: A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom .) (Contributed by Mario Carneiro, 12-Jan-2013) Avoid ax-un . (Revised by BTernaryTau, 30-Dec-2024)

Ref Expression
Assertion 1sdom ( 𝐴 ∈ 𝑉 → ( 1o ≺ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 1sdom2dom ⊢ ( 1o ≺ 𝐴 ↔ 2o ≼ 𝐴 )
2 2dom ⊢ ( 2o ≼ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )
3 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
4 3 2rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )
5 rex2dom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ) → 2o ≼ 𝐴 )
6 4 5 sylan2br ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) → 2o ≼ 𝐴 )
7 6 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 → 2o ≼ 𝐴 ) )
8 2 7 impbid2 ⊢ ( 𝐴 ∈ 𝑉 → ( 2o ≼ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )
9 1 8 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( 1o ≺ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )