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 ≼ 𝐴 )