Step | Hyp | Ref
| Expression |
1 | | prex 5325 |
. . . . . . 7
⊢ {𝐵, 𝐶} ∈ V |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → {𝐵, 𝐶} ∈ V) |
3 | | simpl 486 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → 𝑅 Fr 𝐴) |
4 | | prssi 4734 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → {𝐵, 𝐶} ⊆ 𝐴) |
5 | 4 | adantl 485 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → {𝐵, 𝐶} ⊆ 𝐴) |
6 | | prnzg 4694 |
. . . . . . 7
⊢ (𝐵 ∈ 𝐴 → {𝐵, 𝐶} ≠ ∅) |
7 | 6 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → {𝐵, 𝐶} ≠ ∅) |
8 | | fri 5512 |
. . . . . 6
⊢ ((({𝐵, 𝐶} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝐵, 𝐶} ⊆ 𝐴 ∧ {𝐵, 𝐶} ≠ ∅)) → ∃𝑦 ∈ {𝐵, 𝐶}∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦) |
9 | 2, 3, 5, 7, 8 | syl22anc 839 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ∃𝑦 ∈ {𝐵, 𝐶}∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦) |
10 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝐵)) |
11 | 10 | notbid 321 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝐵)) |
12 | 11 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦 ↔ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵)) |
13 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝑦 = 𝐶 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝐶)) |
14 | 13 | notbid 321 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝐶)) |
15 | 14 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦 ↔ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶)) |
16 | 12, 15 | rexprg 4612 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (∃𝑦 ∈ {𝐵, 𝐶}∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦 ↔ (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 ∨ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶))) |
17 | 16 | adantl 485 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (∃𝑦 ∈ {𝐵, 𝐶}∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝑦 ↔ (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 ∨ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶))) |
18 | 9, 17 | mpbid 235 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 ∨ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶)) |
19 | | prid2g 4677 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐵, 𝐶}) |
20 | 19 | ad2antll 729 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → 𝐶 ∈ {𝐵, 𝐶}) |
21 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → (𝑥𝑅𝐵 ↔ 𝐶𝑅𝐵)) |
22 | 21 | notbid 321 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (¬ 𝑥𝑅𝐵 ↔ ¬ 𝐶𝑅𝐵)) |
23 | 22 | rspcv 3532 |
. . . . . 6
⊢ (𝐶 ∈ {𝐵, 𝐶} → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 → ¬ 𝐶𝑅𝐵)) |
24 | 20, 23 | syl 17 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 → ¬ 𝐶𝑅𝐵)) |
25 | | prid1g 4676 |
. . . . . . 7
⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ {𝐵, 𝐶}) |
26 | 25 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → 𝐵 ∈ {𝐵, 𝐶}) |
27 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
28 | 27 | notbid 321 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (¬ 𝑥𝑅𝐶 ↔ ¬ 𝐵𝑅𝐶)) |
29 | 28 | rspcv 3532 |
. . . . . 6
⊢ (𝐵 ∈ {𝐵, 𝐶} → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶 → ¬ 𝐵𝑅𝐶)) |
30 | 26, 29 | syl 17 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶 → ¬ 𝐵𝑅𝐶)) |
31 | 24, 30 | orim12d 965 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐵 ∨ ∀𝑥 ∈ {𝐵, 𝐶} ¬ 𝑥𝑅𝐶) → (¬ 𝐶𝑅𝐵 ∨ ¬ 𝐵𝑅𝐶))) |
32 | 18, 31 | mpd 15 |
. . 3
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (¬ 𝐶𝑅𝐵 ∨ ¬ 𝐵𝑅𝐶)) |
33 | 32 | orcomd 871 |
. 2
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (¬ 𝐵𝑅𝐶 ∨ ¬ 𝐶𝑅𝐵)) |
34 | | ianor 982 |
. 2
⊢ (¬
(𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵) ↔ (¬ 𝐵𝑅𝐶 ∨ ¬ 𝐶𝑅𝐵)) |
35 | 33, 34 | sylibr 237 |
1
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |