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

Metamath Proof Explorer

Theorem 2dom

Description: A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004)

Ref Expression
Assertion 2dom ( 2o ≼ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )

Proof

Step Hyp Ref Expression
1 df2o2 ⊢ 2o = { ∅ , { ∅ } }
2 1 breq1i ⊢ ( 2o ≼ 𝐴 ↔ { ∅ , { ∅ } } ≼ 𝐴 )
3 brdomi ⊢ ( { ∅ , { ∅ } } ≼ 𝐴 → ∃ 𝑓 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 )
4 2 3 sylbi ⊢ ( 2o ≼ 𝐴 → ∃ 𝑓 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 )
5 f1f ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → 𝑓 : { ∅ , { ∅ } } ⟶ 𝐴 )
6 0ex ⊢ ∅ ∈ V
7 6 prid1 ⊢ ∅ ∈ { ∅ , { ∅ } }
8 ffvelcdm ⊢ ( ( 𝑓 : { ∅ , { ∅ } } ⟶ 𝐴 ∧ ∅ ∈ { ∅ , { ∅ } } ) → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
9 5 7 8 sylancl ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
10 snex ⊢ { ∅ } ∈ V
11 10 prid2 ⊢ { ∅ } ∈ { ∅ , { ∅ } }
12 ffvelcdm ⊢ ( ( 𝑓 : { ∅ , { ∅ } } ⟶ 𝐴 ∧ { ∅ } ∈ { ∅ , { ∅ } } ) → ( 𝑓 ‘ { ∅ } ) ∈ 𝐴 )
13 5 11 12 sylancl ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ( 𝑓 ‘ { ∅ } ) ∈ 𝐴 )
14 0nep0 ⊢ ∅ ≠ { ∅ }
15 14 neii ⊢ ¬ ∅ = { ∅ }
16 f1fveq ⊢ ( ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 ∧ ( ∅ ∈ { ∅ , { ∅ } } ∧ { ∅ } ∈ { ∅ , { ∅ } } ) ) → ( ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) ↔ ∅ = { ∅ } ) )
17 7 11 16 mpanr12 ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ( ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) ↔ ∅ = { ∅ } ) )
18 15 17 mtbiri ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ¬ ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) )
19 eqeq1 ⊢ ( 𝑥 = ( 𝑓 ‘ ∅ ) → ( 𝑥 = 𝑦 ↔ ( 𝑓 ‘ ∅ ) = 𝑦 ) )
20 19 notbid ⊢ ( 𝑥 = ( 𝑓 ‘ ∅ ) → ( ¬ 𝑥 = 𝑦 ↔ ¬ ( 𝑓 ‘ ∅ ) = 𝑦 ) )
21 eqeq2 ⊢ ( 𝑦 = ( 𝑓 ‘ { ∅ } ) → ( ( 𝑓 ‘ ∅ ) = 𝑦 ↔ ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) ) )
22 21 notbid ⊢ ( 𝑦 = ( 𝑓 ‘ { ∅ } ) → ( ¬ ( 𝑓 ‘ ∅ ) = 𝑦 ↔ ¬ ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) ) )
23 20 22 rspc2ev ⊢ ( ( ( 𝑓 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝑓 ‘ { ∅ } ) ∈ 𝐴 ∧ ¬ ( 𝑓 ‘ ∅ ) = ( 𝑓 ‘ { ∅ } ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )
24 9 13 18 23 syl3anc ⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )
25 24 exlimiv ⊢ ( ∃ 𝑓 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )
26 4 25 syl ⊢ ( 2o ≼ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )