Step |
Hyp |
Ref |
Expression |
1 |
|
tpex |
|- { B , C , D } e. _V |
2 |
1
|
a1i |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } e. _V ) |
3 |
|
simpl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> R Fr A ) |
4 |
|
df-tp |
|- { B , C , D } = ( { B , C } u. { D } ) |
5 |
|
simpr1 |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> B e. A ) |
6 |
|
simpr2 |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> C e. A ) |
7 |
5 6
|
prssd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C } C_ A ) |
8 |
|
simpr3 |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> D e. A ) |
9 |
8
|
snssd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { D } C_ A ) |
10 |
7 9
|
unssd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( { B , C } u. { D } ) C_ A ) |
11 |
4 10
|
eqsstrid |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } C_ A ) |
12 |
5
|
tpnzd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } =/= (/) ) |
13 |
|
fri |
|- ( ( ( { B , C , D } e. _V /\ R Fr A ) /\ ( { B , C , D } C_ A /\ { B , C , D } =/= (/) ) ) -> E. x e. { B , C , D } A. y e. { B , C , D } -. y R x ) |
14 |
2 3 11 12 13
|
syl22anc |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> E. x e. { B , C , D } A. y e. { B , C , D } -. y R x ) |
15 |
|
breq2 |
|- ( x = B -> ( y R x <-> y R B ) ) |
16 |
15
|
notbid |
|- ( x = B -> ( -. y R x <-> -. y R B ) ) |
17 |
16
|
ralbidv |
|- ( x = B -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { B , C , D } -. y R B ) ) |
18 |
|
breq2 |
|- ( x = C -> ( y R x <-> y R C ) ) |
19 |
18
|
notbid |
|- ( x = C -> ( -. y R x <-> -. y R C ) ) |
20 |
19
|
ralbidv |
|- ( x = C -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { B , C , D } -. y R C ) ) |
21 |
|
breq2 |
|- ( x = D -> ( y R x <-> y R D ) ) |
22 |
21
|
notbid |
|- ( x = D -> ( -. y R x <-> -. y R D ) ) |
23 |
22
|
ralbidv |
|- ( x = D -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { B , C , D } -. y R D ) ) |
24 |
17 20 23
|
rextpg |
|- ( ( B e. A /\ C e. A /\ D e. A ) -> ( E. x e. { B , C , D } A. y e. { B , C , D } -. y R x <-> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) ) ) |
25 |
24
|
adantl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( E. x e. { B , C , D } A. y e. { B , C , D } -. y R x <-> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) ) ) |
26 |
14 25
|
mpbid |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) ) |
27 |
|
snsstp3 |
|- { D } C_ { B , C , D } |
28 |
|
snssg |
|- ( D e. A -> ( D e. { B , C , D } <-> { D } C_ { B , C , D } ) ) |
29 |
8 28
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( D e. { B , C , D } <-> { D } C_ { B , C , D } ) ) |
30 |
27 29
|
mpbiri |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> D e. { B , C , D } ) |
31 |
|
breq1 |
|- ( y = D -> ( y R B <-> D R B ) ) |
32 |
31
|
notbid |
|- ( y = D -> ( -. y R B <-> -. D R B ) ) |
33 |
32
|
rspcv |
|- ( D e. { B , C , D } -> ( A. y e. { B , C , D } -. y R B -> -. D R B ) ) |
34 |
30 33
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R B -> -. D R B ) ) |
35 |
|
snsstp1 |
|- { B } C_ { B , C , D } |
36 |
|
snssg |
|- ( B e. A -> ( B e. { B , C , D } <-> { B } C_ { B , C , D } ) ) |
37 |
5 36
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( B e. { B , C , D } <-> { B } C_ { B , C , D } ) ) |
38 |
35 37
|
mpbiri |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> B e. { B , C , D } ) |
39 |
|
breq1 |
|- ( y = B -> ( y R C <-> B R C ) ) |
40 |
39
|
notbid |
|- ( y = B -> ( -. y R C <-> -. B R C ) ) |
41 |
40
|
rspcv |
|- ( B e. { B , C , D } -> ( A. y e. { B , C , D } -. y R C -> -. B R C ) ) |
42 |
38 41
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R C -> -. B R C ) ) |
43 |
|
snsstp2 |
|- { C } C_ { B , C , D } |
44 |
|
snssg |
|- ( C e. A -> ( C e. { B , C , D } <-> { C } C_ { B , C , D } ) ) |
45 |
6 44
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( C e. { B , C , D } <-> { C } C_ { B , C , D } ) ) |
46 |
43 45
|
mpbiri |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> C e. { B , C , D } ) |
47 |
|
breq1 |
|- ( y = C -> ( y R D <-> C R D ) ) |
48 |
47
|
notbid |
|- ( y = C -> ( -. y R D <-> -. C R D ) ) |
49 |
48
|
rspcv |
|- ( C e. { B , C , D } -> ( A. y e. { B , C , D } -. y R D -> -. C R D ) ) |
50 |
46 49
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R D -> -. C R D ) ) |
51 |
34 42 50
|
3orim123d |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) -> ( -. D R B \/ -. B R C \/ -. C R D ) ) ) |
52 |
26 51
|
mpd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( -. D R B \/ -. B R C \/ -. C R D ) ) |
53 |
|
3ianor |
|- ( -. ( D R B /\ B R C /\ C R D ) <-> ( -. D R B \/ -. B R C \/ -. C R D ) ) |
54 |
52 53
|
sylibr |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( D R B /\ B R C /\ C R D ) ) |
55 |
|
3anrot |
|- ( ( D R B /\ B R C /\ C R D ) <-> ( B R C /\ C R D /\ D R B ) ) |
56 |
54 55
|
sylnib |
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) ) |