| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df2o2 8515 | . . . 4
⊢
2o = {∅, {∅}} | 
| 2 | 1 | breq1i 5150 | . . 3
⊢
(2o ≼ 𝐴 ↔ {∅, {∅}} ≼ 𝐴) | 
| 3 |  | brdomi 8999 | . . 3
⊢
({∅, {∅}} ≼ 𝐴 → ∃𝑓 𝑓:{∅, {∅}}–1-1→𝐴) | 
| 4 | 2, 3 | sylbi 217 | . 2
⊢
(2o ≼ 𝐴 → ∃𝑓 𝑓:{∅, {∅}}–1-1→𝐴) | 
| 5 |  | f1f 6804 | . . . . 5
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → 𝑓:{∅, {∅}}⟶𝐴) | 
| 6 |  | 0ex 5307 | . . . . . 6
⊢ ∅
∈ V | 
| 7 | 6 | prid1 4762 | . . . . 5
⊢ ∅
∈ {∅, {∅}} | 
| 8 |  | ffvelcdm 7101 | . . . . 5
⊢ ((𝑓:{∅,
{∅}}⟶𝐴 ∧
∅ ∈ {∅, {∅}}) → (𝑓‘∅) ∈ 𝐴) | 
| 9 | 5, 7, 8 | sylancl 586 | . . . 4
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → (𝑓‘∅) ∈ 𝐴) | 
| 10 |  | snex 5436 | . . . . . 6
⊢ {∅}
∈ V | 
| 11 | 10 | prid2 4763 | . . . . 5
⊢ {∅}
∈ {∅, {∅}} | 
| 12 |  | ffvelcdm 7101 | . . . . 5
⊢ ((𝑓:{∅,
{∅}}⟶𝐴 ∧
{∅} ∈ {∅, {∅}}) → (𝑓‘{∅}) ∈ 𝐴) | 
| 13 | 5, 11, 12 | sylancl 586 | . . . 4
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → (𝑓‘{∅}) ∈ 𝐴) | 
| 14 |  | 0nep0 5358 | . . . . . 6
⊢ ∅
≠ {∅} | 
| 15 | 14 | neii 2942 | . . . . 5
⊢  ¬
∅ = {∅} | 
| 16 |  | f1fveq 7282 | . . . . . 6
⊢ ((𝑓:{∅,
{∅}}–1-1→𝐴 ∧ (∅ ∈ {∅,
{∅}} ∧ {∅} ∈ {∅, {∅}})) → ((𝑓‘∅) = (𝑓‘{∅}) ↔ ∅
= {∅})) | 
| 17 | 7, 11, 16 | mpanr12 705 | . . . . 5
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → ((𝑓‘∅) = (𝑓‘{∅}) ↔ ∅ =
{∅})) | 
| 18 | 15, 17 | mtbiri 327 | . . . 4
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → ¬ (𝑓‘∅) = (𝑓‘{∅})) | 
| 19 |  | eqeq1 2741 | . . . . . 6
⊢ (𝑥 = (𝑓‘∅) → (𝑥 = 𝑦 ↔ (𝑓‘∅) = 𝑦)) | 
| 20 | 19 | notbid 318 | . . . . 5
⊢ (𝑥 = (𝑓‘∅) → (¬ 𝑥 = 𝑦 ↔ ¬ (𝑓‘∅) = 𝑦)) | 
| 21 |  | eqeq2 2749 | . . . . . 6
⊢ (𝑦 = (𝑓‘{∅}) → ((𝑓‘∅) = 𝑦 ↔ (𝑓‘∅) = (𝑓‘{∅}))) | 
| 22 | 21 | notbid 318 | . . . . 5
⊢ (𝑦 = (𝑓‘{∅}) → (¬ (𝑓‘∅) = 𝑦 ↔ ¬ (𝑓‘∅) = (𝑓‘{∅}))) | 
| 23 | 20, 22 | rspc2ev 3635 | . . . 4
⊢ (((𝑓‘∅) ∈ 𝐴 ∧ (𝑓‘{∅}) ∈ 𝐴 ∧ ¬ (𝑓‘∅) = (𝑓‘{∅})) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | 
| 24 | 9, 13, 18, 23 | syl3anc 1373 | . . 3
⊢ (𝑓:{∅,
{∅}}–1-1→𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | 
| 25 | 24 | exlimiv 1930 | . 2
⊢
(∃𝑓 𝑓:{∅,
{∅}}–1-1→𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | 
| 26 | 4, 25 | syl 17 | 1
⊢
(2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) |