Proof of Theorem fiinfg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fiming 9538 | . 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦)) | 
| 2 |  | equcom 2017 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | 
| 3 |  | sotrieq2 5624 | . . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑦 = 𝑥 ↔ (¬ 𝑦𝑅𝑥 ∧ ¬ 𝑥𝑅𝑦))) | 
| 4 | 3 | ancom2s 650 | . . . . . . . . . . . 12
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 = 𝑥 ↔ (¬ 𝑦𝑅𝑥 ∧ ¬ 𝑥𝑅𝑦))) | 
| 5 | 2, 4 | bitrid 283 | . . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 = 𝑦 ↔ (¬ 𝑦𝑅𝑥 ∧ ¬ 𝑥𝑅𝑦))) | 
| 6 | 5 | simprbda 498 | . . . . . . . . . 10
⊢ (((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑥 = 𝑦) → ¬ 𝑦𝑅𝑥) | 
| 7 | 6 | ex 412 | . . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 = 𝑦 → ¬ 𝑦𝑅𝑥)) | 
| 8 | 7 | anassrs 467 | . . . . . . . 8
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 = 𝑦 → ¬ 𝑦𝑅𝑥)) | 
| 9 | 8 | a1dd 50 | . . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 = 𝑦 → ((𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ¬ 𝑦𝑅𝑥))) | 
| 10 |  | pm2.27 42 | . . . . . . . 8
⊢ (𝑥 ≠ 𝑦 → ((𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → 𝑥𝑅𝑦)) | 
| 11 |  | soasym 5625 | . . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 → ¬ 𝑦𝑅𝑥)) | 
| 12 | 11 | anassrs 467 | . . . . . . . 8
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 → ¬ 𝑦𝑅𝑥)) | 
| 13 | 10, 12 | syl9r 78 | . . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≠ 𝑦 → ((𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ¬ 𝑦𝑅𝑥))) | 
| 14 | 9, 13 | pm2.61dne 3028 | . . . . . 6
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ¬ 𝑦𝑅𝑥)) | 
| 15 | 14 | ralimdva 3167 | . . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)) | 
| 16 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧𝑅𝑦 ↔ 𝑥𝑅𝑦)) | 
| 17 | 16 | rspcev 3622 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦) → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦) | 
| 18 | 17 | ex 412 | . . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)) | 
| 19 | 18 | ralrimivw 3150 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)) | 
| 20 | 19 | adantl 481 | . . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)) | 
| 21 | 15, 20 | jctird 526 | . . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)))) | 
| 22 | 21 | reximdva 3168 | . . 3
⊢ (𝑅 Or 𝐴 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)))) | 
| 23 | 22 | 3ad2ant1 1134 | . 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)))) | 
| 24 | 1, 23 | mpd 15 | 1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦))) |