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		ffvelrn	⊢ ( ( 𝑓 : { ∅ , { ∅ } } ⟶ 𝐴 ∧ ∅ ∈ { ∅ , { ∅ } } ) → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
9	5 7 8	sylancl	⊢ ( 𝑓 : { ∅ , { ∅ } } –1-1→ 𝐴 → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
10		snex	⊢ { ∅ } ∈ V
11	10	prid2	⊢ { ∅ } ∈ { ∅ , { ∅ } }
12		ffvelrn	⊢ ( ( 𝑓 : { ∅ , { ∅ } } ⟶ 𝐴 ∧ { ∅ } ∈ { ∅ , { ∅ } } ) → ( 𝑓 ‘ { ∅ } ) ∈ 𝐴 )
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 ≼ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 )