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 ≺ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )