Metamath Proof Explorer

Theorem prproropf1olem4

Description: Lemma 4 for prproropf1o . (Contributed by AV, 14-Mar-2023)

Ref Expression
Hypotheses prproropf1o.o 
|- O = ( R i^i ( V X. V ) )
prproropf1o.p 
|- P = { p e. ~P V | ( # ` p ) = 2 }
prproropf1o.f 
|- F = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
Assertion prproropf1olem4 
|- ( ( R Or V /\ W e. P /\ Z e. P ) -> ( ( F ` Z ) = ( F ` W ) -> Z = W ) )

Proof

Step Hyp Ref Expression
1 prproropf1o.o 
 |-  O = ( R i^i ( V X. V ) )
2 prproropf1o.p 
 |-  P = { p e. ~P V | ( # ` p ) = 2 }
3 prproropf1o.f 
 |-  F = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
4 infeq1 
 |-  ( p = Z -> inf ( p , V , R ) = inf ( Z , V , R ) )
5 supeq1 
 |-  ( p = Z -> sup ( p , V , R ) = sup ( Z , V , R ) )
6 4 5 opeq12d 
 |-  ( p = Z -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( Z , V , R ) , sup ( Z , V , R ) >. )
7 simp3 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> Z e. P )
8 opex 
 |-  <. inf ( Z , V , R ) , sup ( Z , V , R ) >. e. _V
9 8 a1i 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> <. inf ( Z , V , R ) , sup ( Z , V , R ) >. e. _V )
10 3 6 7 9 fvmptd3 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> ( F ` Z ) = <. inf ( Z , V , R ) , sup ( Z , V , R ) >. )
11 infeq1 
 |-  ( p = W -> inf ( p , V , R ) = inf ( W , V , R ) )
12 supeq1 
 |-  ( p = W -> sup ( p , V , R ) = sup ( W , V , R ) )
13 11 12 opeq12d 
 |-  ( p = W -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. )
14 simp2 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> W e. P )
15 opex 
 |-  <. inf ( W , V , R ) , sup ( W , V , R ) >. e. _V
16 15 a1i 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> <. inf ( W , V , R ) , sup ( W , V , R ) >. e. _V )
17 3 13 14 16 fvmptd3 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> ( F ` W ) = <. inf ( W , V , R ) , sup ( W , V , R ) >. )
18 10 17 eqeq12d 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> ( ( F ` Z ) = ( F ` W ) <-> <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. ) )
19 2 prpair 
 |-  ( Z e. P <-> E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) )
20 2 prpair 
 |-  ( W e. P <-> E. a e. V E. b e. V ( W = { a , b } /\ a =/= b ) )
21 id 
 |-  ( R Or V -> R Or V )
22 21 infexd 
 |-  ( R Or V -> inf ( { c , d } , V , R ) e. _V )
23 21 supexd 
 |-  ( R Or V -> sup ( { c , d } , V , R ) e. _V )
24 22 23 jca 
 |-  ( R Or V -> ( inf ( { c , d } , V , R ) e. _V /\ sup ( { c , d } , V , R ) e. _V ) )
25 24 ad4antr 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( inf ( { c , d } , V , R ) e. _V /\ sup ( { c , d } , V , R ) e. _V ) )
26 opthg 
 |-  ( ( inf ( { c , d } , V , R ) e. _V /\ sup ( { c , d } , V , R ) e. _V ) -> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. <-> ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) ) )
27 25 26 syl 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. <-> ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) ) )
28 solin 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a R b \/ a = b \/ b R a ) )
29 infpr 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> inf ( { a , b } , V , R ) = if ( a R b , a , b ) )
30 29 3expb 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> inf ( { a , b } , V , R ) = if ( a R b , a , b ) )
31 iftrue 
 |-  ( a R b -> if ( a R b , a , b ) = a )
32 30 31 sylan9eqr 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> inf ( { a , b } , V , R ) = a )
33 32 eqeq2d 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) <-> inf ( { c , d } , V , R ) = a ) )
34 suppr 
 |-  ( ( R Or V /\ a e. V /\ b e. V ) -> sup ( { a , b } , V , R ) = if ( b R a , a , b ) )
35 34 3expb 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> sup ( { a , b } , V , R ) = if ( b R a , a , b ) )
36 35 adantl 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> sup ( { a , b } , V , R ) = if ( b R a , a , b ) )
37 sotric 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a R b <-> -. ( a = b \/ b R a ) ) )
38 ioran 
 |-  ( -. ( a = b \/ b R a ) <-> ( -. a = b /\ -. b R a ) )
39 iffalse 
 |-  ( -. b R a -> if ( b R a , a , b ) = b )
40 38 39 simplbiim 
 |-  ( -. ( a = b \/ b R a ) -> if ( b R a , a , b ) = b )
41 37 40 biimtrdi 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a R b -> if ( b R a , a , b ) = b ) )
42 41 impcom 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> if ( b R a , a , b ) = b )
43 36 42 eqtrd 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> sup ( { a , b } , V , R ) = b )
44 43 eqeq2d 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) <-> sup ( { c , d } , V , R ) = b ) )
45 33 44 anbi12d 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) <-> ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) ) )
46 45 adantr 
 |-  ( ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) <-> ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) ) )
47 solin 
 |-  ( ( R Or V /\ ( c e. V /\ d e. V ) ) -> ( c R d \/ c = d \/ d R c ) )
48 47 adantrr 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( c R d \/ c = d \/ d R c ) )
49 simpl 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> R Or V )
50 simprll 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> c e. V )
51 simprlr 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> d e. V )
52 infpr 
 |-  ( ( R Or V /\ c e. V /\ d e. V ) -> inf ( { c , d } , V , R ) = if ( c R d , c , d ) )
53 49 50 51 52 syl3anc 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> inf ( { c , d } , V , R ) = if ( c R d , c , d ) )
54 iftrue 
 |-  ( c R d -> if ( c R d , c , d ) = c )
55 53 54 sylan9eqr 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> inf ( { c , d } , V , R ) = c )
56 55 eqeq1d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( inf ( { c , d } , V , R ) = a <-> c = a ) )
57 suppr 
 |-  ( ( R Or V /\ c e. V /\ d e. V ) -> sup ( { c , d } , V , R ) = if ( d R c , c , d ) )
58 49 50 51 57 syl3anc 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> sup ( { c , d } , V , R ) = if ( d R c , c , d ) )
59 58 adantl 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> sup ( { c , d } , V , R ) = if ( d R c , c , d ) )
60 sotric 
 |-  ( ( R Or V /\ ( c e. V /\ d e. V ) ) -> ( c R d <-> -. ( c = d \/ d R c ) ) )
61 60 adantrr 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( c R d <-> -. ( c = d \/ d R c ) ) )
62 ioran 
 |-  ( -. ( c = d \/ d R c ) <-> ( -. c = d /\ -. d R c ) )
63 iffalse 
 |-  ( -. d R c -> if ( d R c , c , d ) = d )
64 62 63 simplbiim 
 |-  ( -. ( c = d \/ d R c ) -> if ( d R c , c , d ) = d )
65 61 64 biimtrdi 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( c R d -> if ( d R c , c , d ) = d ) )
66 65 impcom 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> if ( d R c , c , d ) = d )
67 59 66 eqtrd 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> sup ( { c , d } , V , R ) = d )
68 67 eqeq1d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( sup ( { c , d } , V , R ) = b <-> d = b ) )
69 56 68 anbi12d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) <-> ( c = a /\ d = b ) ) )
70 orc 
 |-  ( ( c = a /\ d = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) )
71 69 70 biimtrdi 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
72 71 ex 
 |-  ( c R d -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
73 eqneqall 
 |-  ( c = d -> ( c =/= d -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
74 73 adantld 
 |-  ( c = d -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
75 74 adantld 
 |-  ( c = d -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
76 53 adantl 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> inf ( { c , d } , V , R ) = if ( c R d , c , d ) )
77 76 eqeq1d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( inf ( { c , d } , V , R ) = a <-> if ( c R d , c , d ) = a ) )
78 iftrue 
 |-  ( d R c -> if ( d R c , c , d ) = c )
79 58 78 sylan9eqr 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> sup ( { c , d } , V , R ) = c )
80 79 eqeq1d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( sup ( { c , d } , V , R ) = b <-> c = b ) )
81 77 80 anbi12d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) <-> ( if ( c R d , c , d ) = a /\ c = b ) ) )
82 simpl 
 |-  ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( c e. V /\ d e. V ) )
83 82 ancomd 
 |-  ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( d e. V /\ c e. V ) )
84 sotric 
 |-  ( ( R Or V /\ ( d e. V /\ c e. V ) ) -> ( d R c <-> -. ( d = c \/ c R d ) ) )
85 83 84 sylan2 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( d R c <-> -. ( d = c \/ c R d ) ) )
86 ioran 
 |-  ( -. ( d = c \/ c R d ) <-> ( -. d = c /\ -. c R d ) )
87 iffalse 
 |-  ( -. c R d -> if ( c R d , c , d ) = d )
88 86 87 simplbiim 
 |-  ( -. ( d = c \/ c R d ) -> if ( c R d , c , d ) = d )
89 88 eqeq1d 
 |-  ( -. ( d = c \/ c R d ) -> ( if ( c R d , c , d ) = a <-> d = a ) )
90 85 89 biimtrdi 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( d R c -> ( if ( c R d , c , d ) = a <-> d = a ) ) )
91 90 impcom 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( if ( c R d , c , d ) = a <-> d = a ) )
92 91 anbi1d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( if ( c R d , c , d ) = a /\ c = b ) <-> ( d = a /\ c = b ) ) )
93 olc 
 |-  ( ( c = b /\ d = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) )
94 93 ancoms 
 |-  ( ( d = a /\ c = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) )
95 92 94 biimtrdi 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( if ( c R d , c , d ) = a /\ c = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
96 81 95 sylbid 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
97 96 ex 
 |-  ( d R c -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
98 72 75 97 3jaoi 
 |-  ( ( c R d \/ c = d \/ d R c ) -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
99 48 98 mpcom 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
100 99 ex 
 |-  ( R Or V -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
101 100 ad2antrl 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
102 101 imp 
 |-  ( ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = a /\ sup ( { c , d } , V , R ) = b ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
103 46 102 sylbid 
 |-  ( ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
104 103 ex 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
105 104 a1d 
 |-  ( ( a R b /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) )
106 105 ex 
 |-  ( a R b -> ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) ) )
107 eqneqall 
 |-  ( a = b -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) )
108 107 a1d 
 |-  ( a = b -> ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) ) )
109 30 adantl 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> inf ( { a , b } , V , R ) = if ( a R b , a , b ) )
110 sotric 
 |-  ( ( R Or V /\ ( b e. V /\ a e. V ) ) -> ( b R a <-> -. ( b = a \/ a R b ) ) )
111 110 ancom2s 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( b R a <-> -. ( b = a \/ a R b ) ) )
112 ioran 
 |-  ( -. ( b = a \/ a R b ) <-> ( -. b = a /\ -. a R b ) )
113 iffalse 
 |-  ( -. a R b -> if ( a R b , a , b ) = b )
114 112 113 simplbiim 
 |-  ( -. ( b = a \/ a R b ) -> if ( a R b , a , b ) = b )
115 111 114 biimtrdi 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( b R a -> if ( a R b , a , b ) = b ) )
116 115 impcom 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> if ( a R b , a , b ) = b )
117 109 116 eqtrd 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> inf ( { a , b } , V , R ) = b )
118 117 eqeq2d 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) <-> inf ( { c , d } , V , R ) = b ) )
119 iftrue 
 |-  ( b R a -> if ( b R a , a , b ) = a )
120 35 119 sylan9eqr 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> sup ( { a , b } , V , R ) = a )
121 120 eqeq2d 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) <-> sup ( { c , d } , V , R ) = a ) )
122 118 121 anbi12d 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) <-> ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) ) )
123 122 adantr 
 |-  ( ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) <-> ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) ) )
124 55 eqeq1d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( inf ( { c , d } , V , R ) = b <-> c = b ) )
125 67 eqeq1d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( sup ( { c , d } , V , R ) = a <-> d = a ) )
126 124 125 anbi12d 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) <-> ( c = b /\ d = a ) ) )
127 126 93 biimtrdi 
 |-  ( ( c R d /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
128 127 ex 
 |-  ( c R d -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
129 eqneqall 
 |-  ( c = d -> ( c =/= d -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
130 129 adantld 
 |-  ( c = d -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
131 130 adantld 
 |-  ( c = d -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
132 85 88 biimtrdi 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( d R c -> if ( c R d , c , d ) = d ) )
133 132 impcom 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> if ( c R d , c , d ) = d )
134 76 133 eqtrd 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> inf ( { c , d } , V , R ) = d )
135 134 eqeq1d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( inf ( { c , d } , V , R ) = b <-> d = b ) )
136 79 eqeq1d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( sup ( { c , d } , V , R ) = a <-> c = a ) )
137 135 136 anbi12d 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) <-> ( d = b /\ c = a ) ) )
138 70 ancoms 
 |-  ( ( d = b /\ c = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) )
139 137 138 biimtrdi 
 |-  ( ( d R c /\ ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
140 139 ex 
 |-  ( d R c -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
141 128 131 140 3jaoi 
 |-  ( ( c R d \/ c = d \/ d R c ) -> ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
142 48 141 mpcom 
 |-  ( ( R Or V /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
143 142 ex 
 |-  ( R Or V -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
144 143 ad2antrl 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
145 144 imp 
 |-  ( ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = b /\ sup ( { c , d } , V , R ) = a ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
146 123 145 sylbid 
 |-  ( ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) /\ ( ( c e. V /\ d e. V ) /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
147 146 ex 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
148 147 a1d 
 |-  ( ( b R a /\ ( R Or V /\ ( a e. V /\ b e. V ) ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) )
149 148 ex 
 |-  ( b R a -> ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) ) )
150 106 108 149 3jaoi 
 |-  ( ( a R b \/ a = b \/ b R a ) -> ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) ) )
151 28 150 mpcom 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( a =/= b -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) )
152 151 adantld 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( ( W = { a , b } /\ a =/= b ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) ) )
153 152 imp 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) -> ( ( ( c e. V /\ d e. V ) /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
154 153 expdimp 
 |-  ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( c =/= d -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
155 154 adantld 
 |-  ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( ( Z = { c , d } /\ c =/= d ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) ) )
156 155 imp 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) ) )
157 vex 
 |-  c e. _V
158 vex 
 |-  d e. _V
159 vex 
 |-  a e. _V
160 vex 
 |-  b e. _V
161 157 158 159 160 preq12b 
 |-  ( { c , d } = { a , b } <-> ( ( c = a /\ d = b ) \/ ( c = b /\ d = a ) ) )
162 156 161 imbitrrdi 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( ( inf ( { c , d } , V , R ) = inf ( { a , b } , V , R ) /\ sup ( { c , d } , V , R ) = sup ( { a , b } , V , R ) ) -> { c , d } = { a , b } ) )
163 27 162 sylbid 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) )
164 infeq1 
 |-  ( Z = { c , d } -> inf ( Z , V , R ) = inf ( { c , d } , V , R ) )
165 supeq1 
 |-  ( Z = { c , d } -> sup ( Z , V , R ) = sup ( { c , d } , V , R ) )
166 164 165 opeq12d 
 |-  ( Z = { c , d } -> <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. )
167 infeq1 
 |-  ( W = { a , b } -> inf ( W , V , R ) = inf ( { a , b } , V , R ) )
168 supeq1 
 |-  ( W = { a , b } -> sup ( W , V , R ) = sup ( { a , b } , V , R ) )
169 167 168 opeq12d 
 |-  ( W = { a , b } -> <. inf ( W , V , R ) , sup ( W , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. )
170 166 169 eqeqan12rd 
 |-  ( ( W = { a , b } /\ Z = { c , d } ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. <-> <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. ) )
171 eqeq12 
 |-  ( ( Z = { c , d } /\ W = { a , b } ) -> ( Z = W <-> { c , d } = { a , b } ) )
172 171 ancoms 
 |-  ( ( W = { a , b } /\ Z = { c , d } ) -> ( Z = W <-> { c , d } = { a , b } ) )
173 170 172 imbi12d 
 |-  ( ( W = { a , b } /\ Z = { c , d } ) -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) )
174 173 ex 
 |-  ( W = { a , b } -> ( Z = { c , d } -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) ) )
175 174 ad2antrl 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) -> ( Z = { c , d } -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) ) )
176 175 adantr 
 |-  ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( Z = { c , d } -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) ) )
177 176 com12 
 |-  ( Z = { c , d } -> ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) ) )
178 177 adantr 
 |-  ( ( Z = { c , d } /\ c =/= d ) -> ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) ) )
179 178 impcom 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) <-> ( <. inf ( { c , d } , V , R ) , sup ( { c , d } , V , R ) >. = <. inf ( { a , b } , V , R ) , sup ( { a , b } , V , R ) >. -> { c , d } = { a , b } ) ) )
180 163 179 mpbird 
 |-  ( ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) /\ ( Z = { c , d } /\ c =/= d ) ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) )
181 180 ex 
 |-  ( ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) /\ ( c e. V /\ d e. V ) ) -> ( ( Z = { c , d } /\ c =/= d ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) )
182 181 rexlimdvva 
 |-  ( ( ( R Or V /\ ( a e. V /\ b e. V ) ) /\ ( W = { a , b } /\ a =/= b ) ) -> ( E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) )
183 182 ex 
 |-  ( ( R Or V /\ ( a e. V /\ b e. V ) ) -> ( ( W = { a , b } /\ a =/= b ) -> ( E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) ) )
184 183 rexlimdvva 
 |-  ( R Or V -> ( E. a e. V E. b e. V ( W = { a , b } /\ a =/= b ) -> ( E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) ) )
185 184 com13 
 |-  ( E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) -> ( E. a e. V E. b e. V ( W = { a , b } /\ a =/= b ) -> ( R Or V -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) ) )
186 20 185 biimtrid 
 |-  ( E. c e. V E. d e. V ( Z = { c , d } /\ c =/= d ) -> ( W e. P -> ( R Or V -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) ) )
187 19 186 sylbi 
 |-  ( Z e. P -> ( W e. P -> ( R Or V -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) ) ) )
188 187 3imp31 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> ( <. inf ( Z , V , R ) , sup ( Z , V , R ) >. = <. inf ( W , V , R ) , sup ( W , V , R ) >. -> Z = W ) )
189 18 188 sylbid 
 |-  ( ( R Or V /\ W e. P /\ Z e. P ) -> ( ( F ` Z ) = ( F ` W ) -> Z = W ) )