Step |
Hyp |
Ref |
Expression |
1 |
|
prex |
|- { B , C } e. _V |
2 |
1
|
a1i |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } e. _V ) |
3 |
|
simpl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> R Fr A ) |
4 |
|
prssi |
|- ( ( B e. A /\ C e. A ) -> { B , C } C_ A ) |
5 |
4
|
adantl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } C_ A ) |
6 |
|
prnzg |
|- ( B e. A -> { B , C } =/= (/) ) |
7 |
6
|
ad2antrl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } =/= (/) ) |
8 |
|
fri |
|- ( ( ( { B , C } e. _V /\ R Fr A ) /\ ( { B , C } C_ A /\ { B , C } =/= (/) ) ) -> E. y e. { B , C } A. x e. { B , C } -. x R y ) |
9 |
2 3 5 7 8
|
syl22anc |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> E. y e. { B , C } A. x e. { B , C } -. x R y ) |
10 |
|
breq2 |
|- ( y = B -> ( x R y <-> x R B ) ) |
11 |
10
|
notbid |
|- ( y = B -> ( -. x R y <-> -. x R B ) ) |
12 |
11
|
ralbidv |
|- ( y = B -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R B ) ) |
13 |
|
breq2 |
|- ( y = C -> ( x R y <-> x R C ) ) |
14 |
13
|
notbid |
|- ( y = C -> ( -. x R y <-> -. x R C ) ) |
15 |
14
|
ralbidv |
|- ( y = C -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R C ) ) |
16 |
12 15
|
rexprg |
|- ( ( B e. A /\ C e. A ) -> ( E. y e. { B , C } A. x e. { B , C } -. x R y <-> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) ) ) |
17 |
16
|
adantl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( E. y e. { B , C } A. x e. { B , C } -. x R y <-> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) ) ) |
18 |
9 17
|
mpbid |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) ) |
19 |
|
prid2g |
|- ( C e. A -> C e. { B , C } ) |
20 |
19
|
ad2antll |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> C e. { B , C } ) |
21 |
|
breq1 |
|- ( x = C -> ( x R B <-> C R B ) ) |
22 |
21
|
notbid |
|- ( x = C -> ( -. x R B <-> -. C R B ) ) |
23 |
22
|
rspcv |
|- ( C e. { B , C } -> ( A. x e. { B , C } -. x R B -> -. C R B ) ) |
24 |
20 23
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R B -> -. C R B ) ) |
25 |
|
prid1g |
|- ( B e. A -> B e. { B , C } ) |
26 |
25
|
ad2antrl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> B e. { B , C } ) |
27 |
|
breq1 |
|- ( x = B -> ( x R C <-> B R C ) ) |
28 |
27
|
notbid |
|- ( x = B -> ( -. x R C <-> -. B R C ) ) |
29 |
28
|
rspcv |
|- ( B e. { B , C } -> ( A. x e. { B , C } -. x R C -> -. B R C ) ) |
30 |
26 29
|
syl |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R C -> -. B R C ) ) |
31 |
24 30
|
orim12d |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) -> ( -. C R B \/ -. B R C ) ) ) |
32 |
18 31
|
mpd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. C R B \/ -. B R C ) ) |
33 |
32
|
orcomd |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. B R C \/ -. C R B ) ) |
34 |
|
ianor |
|- ( -. ( B R C /\ C R B ) <-> ( -. B R C \/ -. C R B ) ) |
35 |
33 34
|
sylibr |
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) ) |