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

Metamath Proof Explorer

Theorem rex2dom

Description: A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024)

Ref Expression
Assertion rex2dom ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ) → 2o ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 prssi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → { 𝑥 , 𝑦 } ⊆ 𝐴 )
3 df2o3 ⊢ 2o = { ∅ , 1o }
4 0ex ⊢ ∅ ∈ V
5 4 a1i ⊢ ( 𝑥 ≠ 𝑦 → ∅ ∈ V )
6 1oex ⊢ 1o ∈ V
7 6 a1i ⊢ ( 𝑥 ≠ 𝑦 → 1o ∈ V )
8 vex ⊢ 𝑥 ∈ V
9 8 a1i ⊢ ( 𝑥 ≠ 𝑦 → 𝑥 ∈ V )
10 vex ⊢ 𝑦 ∈ V
11 10 a1i ⊢ ( 𝑥 ≠ 𝑦 → 𝑦 ∈ V )
12 1n0 ⊢ 1o ≠ ∅
13 12 necomi ⊢ ∅ ≠ 1o
14 13 a1i ⊢ ( 𝑥 ≠ 𝑦 → ∅ ≠ 1o )
15 id ⊢ ( 𝑥 ≠ 𝑦 → 𝑥 ≠ 𝑦 )
16 5 7 9 11 14 15 en2prd ⊢ ( 𝑥 ≠ 𝑦 → { ∅ , 1o } ≈ { 𝑥 , 𝑦 } )
17 3 16 eqbrtrid ⊢ ( 𝑥 ≠ 𝑦 → 2o ≈ { 𝑥 , 𝑦 } )
18 endom ⊢ ( 2o ≈ { 𝑥 , 𝑦 } → 2o ≼ { 𝑥 , 𝑦 } )
19 17 18 syl ⊢ ( 𝑥 ≠ 𝑦 → 2o ≼ { 𝑥 , 𝑦 } )
20 domssr ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ∧ 2o ≼ { 𝑥 , 𝑦 } ) → 2o ≼ 𝐴 )
21 20 3expib ⊢ ( 𝐴 ∈ V → ( ( { 𝑥 , 𝑦 } ⊆ 𝐴 ∧ 2o ≼ { 𝑥 , 𝑦 } ) → 2o ≼ 𝐴 ) )
22 2 19 21 syl2ani ⊢ ( 𝐴 ∈ V → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → 2o ≼ 𝐴 ) )
23 22 expd ⊢ ( 𝐴 ∈ V → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → 2o ≼ 𝐴 ) ) )
24 23 rexlimdvv ⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → 2o ≼ 𝐴 ) )
25 1 24 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → 2o ≼ 𝐴 ) )
26 25 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ) → 2o ≼ 𝐴 )