Step |
Hyp |
Ref |
Expression |
1 |
|
fimaxg |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ) |
2 |
|
sotrieq2 |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 = 𝑦 ↔ ( ¬ 𝑥 𝑅 𝑦 ∧ ¬ 𝑦 𝑅 𝑥 ) ) ) |
3 |
2
|
simprbda |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 = 𝑦 ) → ¬ 𝑥 𝑅 𝑦 ) |
4 |
3
|
ex |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 = 𝑦 → ¬ 𝑥 𝑅 𝑦 ) ) |
5 |
4
|
anassrs |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = 𝑦 → ¬ 𝑥 𝑅 𝑦 ) ) |
6 |
5
|
a1dd |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = 𝑦 → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ¬ 𝑥 𝑅 𝑦 ) ) ) |
7 |
|
pm2.27 |
⊢ ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → 𝑦 𝑅 𝑥 ) ) |
8 |
|
so2nr |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) |
9 |
|
pm3.21 |
⊢ ( 𝑦 𝑅 𝑥 → ( 𝑥 𝑅 𝑦 → ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) ) |
10 |
9
|
con3d |
⊢ ( 𝑦 𝑅 𝑥 → ( ¬ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → ¬ 𝑥 𝑅 𝑦 ) ) |
11 |
8 10
|
syl5com |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ) |
12 |
11
|
anassrs |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 → ¬ 𝑥 𝑅 𝑦 ) ) |
13 |
7 12
|
syl9r |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ¬ 𝑥 𝑅 𝑦 ) ) ) |
14 |
6 13
|
pm2.61dne |
⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ¬ 𝑥 𝑅 𝑦 ) ) |
15 |
14
|
ralimdva |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) ) |
16 |
|
breq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) ) |
17 |
16
|
rspcev |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) |
18 |
17
|
ex |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) |
19 |
18
|
ralrimivw |
⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) |
21 |
15 20
|
jctird |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ) ) |
22 |
21
|
reximdva |
⊢ ( 𝑅 Or 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ) ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ) ) |
24 |
1 23
|
mpd |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ) |