Step |
Hyp |
Ref |
Expression |
1 |
|
sopo |
⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 ) |
2 |
|
cnvpo |
⊢ ( 𝑅 Po 𝐴 ↔ ◡ 𝑅 Po 𝐴 ) |
3 |
1 2
|
sylib |
⊢ ( 𝑅 Or 𝐴 → ◡ 𝑅 Po 𝐴 ) |
4 |
|
frfi |
⊢ ( ( ◡ 𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 Fr 𝐴 ) |
5 |
3 4
|
sylan |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 Fr 𝐴 ) |
6 |
5
|
3adant3 |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ◡ 𝑅 Fr 𝐴 ) |
7 |
|
ssid |
⊢ 𝐴 ⊆ 𝐴 |
8 |
|
fri |
⊢ ( ( ( 𝐴 ∈ Fin ∧ ◡ 𝑅 Fr 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ) |
9 |
7 8
|
mpanr1 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ ◡ 𝑅 Fr 𝐴 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ) |
10 |
9
|
an32s |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ ◡ 𝑅 Fr 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ) |
11 |
|
vex |
⊢ 𝑦 ∈ V |
12 |
|
vex |
⊢ 𝑥 ∈ V |
13 |
11 12
|
brcnv |
⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) |
14 |
13
|
notbii |
⊢ ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 ) |
15 |
14
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) |
16 |
15
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) |
17 |
10 16
|
sylib |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ ◡ 𝑅 Fr 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) |
18 |
17
|
ex |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝑅 Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) ) |
19 |
18
|
3adant1 |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝑅 Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) ) |
20 |
6 19
|
mpd |
⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) |