Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> R Or A ) |
2 |
|
ifcl |
|- ( ( B e. A /\ C e. A ) -> if ( C R B , B , C ) e. A ) |
3 |
2
|
3adant1 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> if ( C R B , B , C ) e. A ) |
4 |
|
ifpr |
|- ( ( B e. A /\ C e. A ) -> if ( C R B , B , C ) e. { B , C } ) |
5 |
4
|
3adant1 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> if ( C R B , B , C ) e. { B , C } ) |
6 |
|
breq1 |
|- ( B = if ( C R B , B , C ) -> ( B R B <-> if ( C R B , B , C ) R B ) ) |
7 |
6
|
notbid |
|- ( B = if ( C R B , B , C ) -> ( -. B R B <-> -. if ( C R B , B , C ) R B ) ) |
8 |
|
breq1 |
|- ( C = if ( C R B , B , C ) -> ( C R B <-> if ( C R B , B , C ) R B ) ) |
9 |
8
|
notbid |
|- ( C = if ( C R B , B , C ) -> ( -. C R B <-> -. if ( C R B , B , C ) R B ) ) |
10 |
|
sonr |
|- ( ( R Or A /\ B e. A ) -> -. B R B ) |
11 |
10
|
3adant3 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> -. B R B ) |
12 |
11
|
adantr |
|- ( ( ( R Or A /\ B e. A /\ C e. A ) /\ C R B ) -> -. B R B ) |
13 |
|
simpr |
|- ( ( ( R Or A /\ B e. A /\ C e. A ) /\ -. C R B ) -> -. C R B ) |
14 |
7 9 12 13
|
ifbothda |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> -. if ( C R B , B , C ) R B ) |
15 |
|
breq1 |
|- ( B = if ( C R B , B , C ) -> ( B R C <-> if ( C R B , B , C ) R C ) ) |
16 |
15
|
notbid |
|- ( B = if ( C R B , B , C ) -> ( -. B R C <-> -. if ( C R B , B , C ) R C ) ) |
17 |
|
breq1 |
|- ( C = if ( C R B , B , C ) -> ( C R C <-> if ( C R B , B , C ) R C ) ) |
18 |
17
|
notbid |
|- ( C = if ( C R B , B , C ) -> ( -. C R C <-> -. if ( C R B , B , C ) R C ) ) |
19 |
|
so2nr |
|- ( ( R Or A /\ ( C e. A /\ B e. A ) ) -> -. ( C R B /\ B R C ) ) |
20 |
19
|
3impb |
|- ( ( R Or A /\ C e. A /\ B e. A ) -> -. ( C R B /\ B R C ) ) |
21 |
20
|
3com23 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> -. ( C R B /\ B R C ) ) |
22 |
|
imnan |
|- ( ( C R B -> -. B R C ) <-> -. ( C R B /\ B R C ) ) |
23 |
21 22
|
sylibr |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> ( C R B -> -. B R C ) ) |
24 |
23
|
imp |
|- ( ( ( R Or A /\ B e. A /\ C e. A ) /\ C R B ) -> -. B R C ) |
25 |
|
sonr |
|- ( ( R Or A /\ C e. A ) -> -. C R C ) |
26 |
25
|
3adant2 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> -. C R C ) |
27 |
26
|
adantr |
|- ( ( ( R Or A /\ B e. A /\ C e. A ) /\ -. C R B ) -> -. C R C ) |
28 |
16 18 24 27
|
ifbothda |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> -. if ( C R B , B , C ) R C ) |
29 |
|
breq2 |
|- ( y = B -> ( if ( C R B , B , C ) R y <-> if ( C R B , B , C ) R B ) ) |
30 |
29
|
notbid |
|- ( y = B -> ( -. if ( C R B , B , C ) R y <-> -. if ( C R B , B , C ) R B ) ) |
31 |
|
breq2 |
|- ( y = C -> ( if ( C R B , B , C ) R y <-> if ( C R B , B , C ) R C ) ) |
32 |
31
|
notbid |
|- ( y = C -> ( -. if ( C R B , B , C ) R y <-> -. if ( C R B , B , C ) R C ) ) |
33 |
30 32
|
ralprg |
|- ( ( B e. A /\ C e. A ) -> ( A. y e. { B , C } -. if ( C R B , B , C ) R y <-> ( -. if ( C R B , B , C ) R B /\ -. if ( C R B , B , C ) R C ) ) ) |
34 |
33
|
3adant1 |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> ( A. y e. { B , C } -. if ( C R B , B , C ) R y <-> ( -. if ( C R B , B , C ) R B /\ -. if ( C R B , B , C ) R C ) ) ) |
35 |
14 28 34
|
mpbir2and |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> A. y e. { B , C } -. if ( C R B , B , C ) R y ) |
36 |
35
|
r19.21bi |
|- ( ( ( R Or A /\ B e. A /\ C e. A ) /\ y e. { B , C } ) -> -. if ( C R B , B , C ) R y ) |
37 |
1 3 5 36
|
supmax |
|- ( ( R Or A /\ B e. A /\ C e. A ) -> sup ( { B , C } , A , R ) = if ( C R B , B , C ) ) |