Step | Hyp | Ref
| Expression |
1 | | tpex 6957 |
. . . . . . 7
⊢ {𝐵, 𝐶, 𝐷} ∈ V |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → {𝐵, 𝐶, 𝐷} ∈ V) |
3 | | simpl 473 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝑅 Fr 𝐴) |
4 | | df-tp 4182 |
. . . . . . 7
⊢ {𝐵, 𝐶, 𝐷} = ({𝐵, 𝐶} ∪ {𝐷}) |
5 | | simpr1 1067 |
. . . . . . . . 9
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐵 ∈ 𝐴) |
6 | | simpr2 1068 |
. . . . . . . . 9
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐶 ∈ 𝐴) |
7 | | prssi 4353 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → {𝐵, 𝐶} ⊆ 𝐴) |
8 | 5, 6, 7 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → {𝐵, 𝐶} ⊆ 𝐴) |
9 | | simpr3 1069 |
. . . . . . . . 9
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐷 ∈ 𝐴) |
10 | 9 | snssd 4340 |
. . . . . . . 8
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → {𝐷} ⊆ 𝐴) |
11 | 8, 10 | unssd 3789 |
. . . . . . 7
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ({𝐵, 𝐶} ∪ {𝐷}) ⊆ 𝐴) |
12 | 4, 11 | syl5eqss 3649 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → {𝐵, 𝐶, 𝐷} ⊆ 𝐴) |
13 | 5 | tpnzd 4314 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → {𝐵, 𝐶, 𝐷} ≠ ∅) |
14 | | fri 5076 |
. . . . . 6
⊢ ((({𝐵, 𝐶, 𝐷} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝐵, 𝐶, 𝐷} ⊆ 𝐴 ∧ {𝐵, 𝐶, 𝐷} ≠ ∅)) → ∃𝑥 ∈ {𝐵, 𝐶, 𝐷}∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥) |
15 | 2, 3, 12, 13, 14 | syl22anc 1327 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ∃𝑥 ∈ {𝐵, 𝐶, 𝐷}∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥) |
16 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐵)) |
17 | 16 | notbid 308 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝐵)) |
18 | 17 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵)) |
19 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = 𝐶 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐶)) |
20 | 19 | notbid 308 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝐶)) |
21 | 20 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶)) |
22 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑥 = 𝐷 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐷)) |
23 | 22 | notbid 308 |
. . . . . . . 8
⊢ (𝑥 = 𝐷 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝐷)) |
24 | 23 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷)) |
25 | 18, 21, 24 | rextpg 4237 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∃𝑥 ∈ {𝐵, 𝐶, 𝐷}∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥 ↔ (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷))) |
26 | 25 | adantl 482 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (∃𝑥 ∈ {𝐵, 𝐶, 𝐷}∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝑥 ↔ (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷))) |
27 | 15, 26 | mpbid 222 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷)) |
28 | | snsstp3 4349 |
. . . . . . 7
⊢ {𝐷} ⊆ {𝐵, 𝐶, 𝐷} |
29 | | snssg 4327 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝐴 → (𝐷 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐷} ⊆ {𝐵, 𝐶, 𝐷})) |
30 | 9, 29 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐷 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐷} ⊆ {𝐵, 𝐶, 𝐷})) |
31 | 28, 30 | mpbiri 248 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐷 ∈ {𝐵, 𝐶, 𝐷}) |
32 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → (𝑦𝑅𝐵 ↔ 𝐷𝑅𝐵)) |
33 | 32 | notbid 308 |
. . . . . . 7
⊢ (𝑦 = 𝐷 → (¬ 𝑦𝑅𝐵 ↔ ¬ 𝐷𝑅𝐵)) |
34 | 33 | rspcv 3305 |
. . . . . 6
⊢ (𝐷 ∈ {𝐵, 𝐶, 𝐷} → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 → ¬ 𝐷𝑅𝐵)) |
35 | 31, 34 | syl 17 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 → ¬ 𝐷𝑅𝐵)) |
36 | | snsstp1 4347 |
. . . . . . 7
⊢ {𝐵} ⊆ {𝐵, 𝐶, 𝐷} |
37 | | snssg 4327 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐵} ⊆ {𝐵, 𝐶, 𝐷})) |
38 | 5, 37 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐵} ⊆ {𝐵, 𝐶, 𝐷})) |
39 | 36, 38 | mpbiri 248 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐵 ∈ {𝐵, 𝐶, 𝐷}) |
40 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
41 | 40 | notbid 308 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (¬ 𝑦𝑅𝐶 ↔ ¬ 𝐵𝑅𝐶)) |
42 | 41 | rspcv 3305 |
. . . . . 6
⊢ (𝐵 ∈ {𝐵, 𝐶, 𝐷} → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 → ¬ 𝐵𝑅𝐶)) |
43 | 39, 42 | syl 17 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 → ¬ 𝐵𝑅𝐶)) |
44 | | snsstp2 4348 |
. . . . . . 7
⊢ {𝐶} ⊆ {𝐵, 𝐶, 𝐷} |
45 | | snssg 4327 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (𝐶 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐶} ⊆ {𝐵, 𝐶, 𝐷})) |
46 | 6, 45 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ∈ {𝐵, 𝐶, 𝐷} ↔ {𝐶} ⊆ {𝐵, 𝐶, 𝐷})) |
47 | 44, 46 | mpbiri 248 |
. . . . . 6
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐶 ∈ {𝐵, 𝐶, 𝐷}) |
48 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝑦𝑅𝐷 ↔ 𝐶𝑅𝐷)) |
49 | 48 | notbid 308 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (¬ 𝑦𝑅𝐷 ↔ ¬ 𝐶𝑅𝐷)) |
50 | 49 | rspcv 3305 |
. . . . . 6
⊢ (𝐶 ∈ {𝐵, 𝐶, 𝐷} → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷 → ¬ 𝐶𝑅𝐷)) |
51 | 47, 50 | syl 17 |
. . . . 5
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷 → ¬ 𝐶𝑅𝐷)) |
52 | 35, 43, 51 | 3orim123d 1407 |
. . . 4
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐵 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐶 ∨ ∀𝑦 ∈ {𝐵, 𝐶, 𝐷} ¬ 𝑦𝑅𝐷) → (¬ 𝐷𝑅𝐵 ∨ ¬ 𝐵𝑅𝐶 ∨ ¬ 𝐶𝑅𝐷))) |
53 | 27, 52 | mpd 15 |
. . 3
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (¬ 𝐷𝑅𝐵 ∨ ¬ 𝐵𝑅𝐶 ∨ ¬ 𝐶𝑅𝐷)) |
54 | | 3ianor 1055 |
. . 3
⊢ (¬
(𝐷𝑅𝐵 ∧ 𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) ↔ (¬ 𝐷𝑅𝐵 ∨ ¬ 𝐵𝑅𝐶 ∨ ¬ 𝐶𝑅𝐷)) |
55 | 53, 54 | sylibr 224 |
. 2
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐷𝑅𝐵 ∧ 𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷)) |
56 | | 3anrot 1043 |
. 2
⊢ ((𝐷𝑅𝐵 ∧ 𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) ↔ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
57 | 55, 56 | sylnib 318 |
1
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |