Step |
Hyp |
Ref |
Expression |
1 |
|
tpex |
⊢ { 𝐵 , 𝐶 , 𝐷 } ∈ V |
2 |
1
|
a1i |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ∈ V ) |
3 |
|
simpl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝑅 Fr 𝐴 ) |
4 |
|
df-tp |
⊢ { 𝐵 , 𝐶 , 𝐷 } = ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) |
5 |
|
simpr1 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 ) |
6 |
|
simpr2 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 ) |
7 |
5 6
|
prssd |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 } ⊆ 𝐴 ) |
8 |
|
simpr3 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐷 ∈ 𝐴 ) |
9 |
8
|
snssd |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐷 } ⊆ 𝐴 ) |
10 |
7 9
|
unssd |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ⊆ 𝐴 ) |
11 |
4 10
|
eqsstrid |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ⊆ 𝐴 ) |
12 |
5
|
tpnzd |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → { 𝐵 , 𝐶 , 𝐷 } ≠ ∅ ) |
13 |
|
fri |
⊢ ( ( ( { 𝐵 , 𝐶 , 𝐷 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝐵 , 𝐶 , 𝐷 } ⊆ 𝐴 ∧ { 𝐵 , 𝐶 , 𝐷 } ≠ ∅ ) ) → ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ) |
14 |
2 3 11 12 13
|
syl22anc |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ) |
15 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐵 ) ) |
16 |
15
|
notbid |
⊢ ( 𝑥 = 𝐵 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐵 ) ) |
17 |
16
|
ralbidv |
⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ) ) |
18 |
|
breq2 |
⊢ ( 𝑥 = 𝐶 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐶 ) ) |
19 |
18
|
notbid |
⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐶 ) ) |
20 |
19
|
ralbidv |
⊢ ( 𝑥 = 𝐶 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ) ) |
21 |
|
breq2 |
⊢ ( 𝑥 = 𝐷 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐷 ) ) |
22 |
21
|
notbid |
⊢ ( 𝑥 = 𝐷 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝐷 ) ) |
23 |
22
|
ralbidv |
⊢ ( 𝑥 = 𝐷 → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) |
24 |
17 20 23
|
rextpg |
⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) ) |
25 |
24
|
adantl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑥 ∈ { 𝐵 , 𝐶 , 𝐷 } ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝑥 ↔ ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) ) |
26 |
14 25
|
mpbid |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) ) |
27 |
|
snsstp3 |
⊢ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 } |
28 |
|
snssg |
⊢ ( 𝐷 ∈ 𝐴 → ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
29 |
8 28
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐷 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
30 |
27 29
|
mpbiri |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } ) |
31 |
|
breq1 |
⊢ ( 𝑦 = 𝐷 → ( 𝑦 𝑅 𝐵 ↔ 𝐷 𝑅 𝐵 ) ) |
32 |
31
|
notbid |
⊢ ( 𝑦 = 𝐷 → ( ¬ 𝑦 𝑅 𝐵 ↔ ¬ 𝐷 𝑅 𝐵 ) ) |
33 |
32
|
rspcv |
⊢ ( 𝐷 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 → ¬ 𝐷 𝑅 𝐵 ) ) |
34 |
30 33
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 → ¬ 𝐷 𝑅 𝐵 ) ) |
35 |
|
snsstp1 |
⊢ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 } |
36 |
|
snssg |
⊢ ( 𝐵 ∈ 𝐴 → ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
37 |
5 36
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐵 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
38 |
35 37
|
mpbiri |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } ) |
39 |
|
breq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) ) |
40 |
39
|
notbid |
⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑦 𝑅 𝐶 ↔ ¬ 𝐵 𝑅 𝐶 ) ) |
41 |
40
|
rspcv |
⊢ ( 𝐵 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) ) |
42 |
38 41
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 → ¬ 𝐵 𝑅 𝐶 ) ) |
43 |
|
snsstp2 |
⊢ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 } |
44 |
|
snssg |
⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
45 |
6 44
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ { 𝐶 } ⊆ { 𝐵 , 𝐶 , 𝐷 } ) ) |
46 |
43 45
|
mpbiri |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } ) |
47 |
|
breq1 |
⊢ ( 𝑦 = 𝐶 → ( 𝑦 𝑅 𝐷 ↔ 𝐶 𝑅 𝐷 ) ) |
48 |
47
|
notbid |
⊢ ( 𝑦 = 𝐶 → ( ¬ 𝑦 𝑅 𝐷 ↔ ¬ 𝐶 𝑅 𝐷 ) ) |
49 |
48
|
rspcv |
⊢ ( 𝐶 ∈ { 𝐵 , 𝐶 , 𝐷 } → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 → ¬ 𝐶 𝑅 𝐷 ) ) |
50 |
46 49
|
syl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 → ¬ 𝐶 𝑅 𝐷 ) ) |
51 |
34 42 50
|
3orim123d |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐵 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐶 ∨ ∀ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐷 } ¬ 𝑦 𝑅 𝐷 ) → ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) ) ) |
52 |
26 51
|
mpd |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) ) |
53 |
|
3ianor |
⊢ ( ¬ ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ↔ ( ¬ 𝐷 𝑅 𝐵 ∨ ¬ 𝐵 𝑅 𝐶 ∨ ¬ 𝐶 𝑅 𝐷 ) ) |
54 |
52 53
|
sylibr |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ) |
55 |
|
3anrot |
⊢ ( ( 𝐷 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ↔ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ) |
56 |
54 55
|
sylnib |
⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ) |