Metamath Proof Explorer

Theorem ordtbaslem

Description: Lemma for ordtbas . In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 
|- X = dom R
ordtval.2 
|- A = ran ( x e. X |-> { y e. X | -. y R x } )
Assertion ordtbaslem 
|- ( R e. TosetRel -> ( fi ` A ) = A )

Proof

Step Hyp Ref Expression
1 ordtval.1 
 |-  X = dom R
2 ordtval.2 
 |-  A = ran ( x e. X |-> { y e. X | -. y R x } )
3 3anrot 
 |-  ( ( y e. X /\ a e. X /\ b e. X ) <-> ( a e. X /\ b e. X /\ y e. X ) )
4 1 tsrlemax 
 |-  ( ( R e. TosetRel /\ ( y e. X /\ a e. X /\ b e. X ) ) -> ( y R if ( a R b , b , a ) <-> ( y R a \/ y R b ) ) )
5 3 4 sylan2br 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X /\ y e. X ) ) -> ( y R if ( a R b , b , a ) <-> ( y R a \/ y R b ) ) )
6 5 3exp2 
 |-  ( R e. TosetRel -> ( a e. X -> ( b e. X -> ( y e. X -> ( y R if ( a R b , b , a ) <-> ( y R a \/ y R b ) ) ) ) ) )
7 6 imp42 
 |-  ( ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) /\ y e. X ) -> ( y R if ( a R b , b , a ) <-> ( y R a \/ y R b ) ) )
8 7 notbid 
 |-  ( ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) /\ y e. X ) -> ( -. y R if ( a R b , b , a ) <-> -. ( y R a \/ y R b ) ) )
9 ioran 
 |-  ( -. ( y R a \/ y R b ) <-> ( -. y R a /\ -. y R b ) )
10 8 9 bitrdi 
 |-  ( ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) /\ y e. X ) -> ( -. y R if ( a R b , b , a ) <-> ( -. y R a /\ -. y R b ) ) )
11 10 rabbidva 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R if ( a R b , b , a ) } = { y e. X | ( -. y R a /\ -. y R b ) } )
12 ifcl 
 |-  ( ( b e. X /\ a e. X ) -> if ( a R b , b , a ) e. X )
13 12 ancoms 
 |-  ( ( a e. X /\ b e. X ) -> if ( a R b , b , a ) e. X )
14 dmexg 
 |-  ( R e. TosetRel -> dom R e. _V )
15 1 14 eqeltrid 
 |-  ( R e. TosetRel -> X e. _V )
16 15 adantr 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> X e. _V )
17 rabexg 
 |-  ( X e. _V -> { y e. X | ( -. y R a /\ -. y R b ) } e. _V )
18 16 17 syl 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | ( -. y R a /\ -. y R b ) } e. _V )
19 11 18 eqeltrd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R if ( a R b , b , a ) } e. _V )
20 eqid 
 |-  ( x e. X |-> { y e. X | -. y R x } ) = ( x e. X |-> { y e. X | -. y R x } )
21 breq2 
 |-  ( x = if ( a R b , b , a ) -> ( y R x <-> y R if ( a R b , b , a ) ) )
22 21 notbid 
 |-  ( x = if ( a R b , b , a ) -> ( -. y R x <-> -. y R if ( a R b , b , a ) ) )
23 22 rabbidv 
 |-  ( x = if ( a R b , b , a ) -> { y e. X | -. y R x } = { y e. X | -. y R if ( a R b , b , a ) } )
24 20 23 elrnmpt1s 
 |-  ( ( if ( a R b , b , a ) e. X /\ { y e. X | -. y R if ( a R b , b , a ) } e. _V ) -> { y e. X | -. y R if ( a R b , b , a ) } e. ran ( x e. X |-> { y e. X | -. y R x } ) )
25 24 2 eleqtrrdi 
 |-  ( ( if ( a R b , b , a ) e. X /\ { y e. X | -. y R if ( a R b , b , a ) } e. _V ) -> { y e. X | -. y R if ( a R b , b , a ) } e. A )
26 13 19 25 syl2an2 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R if ( a R b , b , a ) } e. A )
27 11 26 eqeltrrd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | ( -. y R a /\ -. y R b ) } e. A )
28 27 ralrimivva 
 |-  ( R e. TosetRel -> A. a e. X A. b e. X { y e. X | ( -. y R a /\ -. y R b ) } e. A )
29 rabexg 
 |-  ( X e. _V -> { y e. X | -. y R a } e. _V )
30 15 29 syl 
 |-  ( R e. TosetRel -> { y e. X | -. y R a } e. _V )
31 30 ralrimivw 
 |-  ( R e. TosetRel -> A. a e. X { y e. X | -. y R a } e. _V )
32 breq2 
 |-  ( x = a -> ( y R x <-> y R a ) )
33 32 notbid 
 |-  ( x = a -> ( -. y R x <-> -. y R a ) )
34 33 rabbidv 
 |-  ( x = a -> { y e. X | -. y R x } = { y e. X | -. y R a } )
35 34 cbvmptv 
 |-  ( x e. X |-> { y e. X | -. y R x } ) = ( a e. X |-> { y e. X | -. y R a } )
36 ineq1 
 |-  ( z = { y e. X | -. y R a } -> ( z i^i { y e. X | -. y R b } ) = ( { y e. X | -. y R a } i^i { y e. X | -. y R b } ) )
37 inrab 
 |-  ( { y e. X | -. y R a } i^i { y e. X | -. y R b } ) = { y e. X | ( -. y R a /\ -. y R b ) }
38 36 37 eqtrdi 
 |-  ( z = { y e. X | -. y R a } -> ( z i^i { y e. X | -. y R b } ) = { y e. X | ( -. y R a /\ -. y R b ) } )
39 38 eleq1d 
 |-  ( z = { y e. X | -. y R a } -> ( ( z i^i { y e. X | -. y R b } ) e. A <-> { y e. X | ( -. y R a /\ -. y R b ) } e. A ) )
40 39 ralbidv 
 |-  ( z = { y e. X | -. y R a } -> ( A. b e. X ( z i^i { y e. X | -. y R b } ) e. A <-> A. b e. X { y e. X | ( -. y R a /\ -. y R b ) } e. A ) )
41 35 40 ralrnmptw 
 |-  ( A. a e. X { y e. X | -. y R a } e. _V -> ( A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. b e. X ( z i^i { y e. X | -. y R b } ) e. A <-> A. a e. X A. b e. X { y e. X | ( -. y R a /\ -. y R b ) } e. A ) )
42 31 41 syl 
 |-  ( R e. TosetRel -> ( A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. b e. X ( z i^i { y e. X | -. y R b } ) e. A <-> A. a e. X A. b e. X { y e. X | ( -. y R a /\ -. y R b ) } e. A ) )
43 28 42 mpbird 
 |-  ( R e. TosetRel -> A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. b e. X ( z i^i { y e. X | -. y R b } ) e. A )
44 rabexg 
 |-  ( X e. _V -> { y e. X | -. y R b } e. _V )
45 15 44 syl 
 |-  ( R e. TosetRel -> { y e. X | -. y R b } e. _V )
46 45 ralrimivw 
 |-  ( R e. TosetRel -> A. b e. X { y e. X | -. y R b } e. _V )
47 breq2 
 |-  ( x = b -> ( y R x <-> y R b ) )
48 47 notbid 
 |-  ( x = b -> ( -. y R x <-> -. y R b ) )
49 48 rabbidv 
 |-  ( x = b -> { y e. X | -. y R x } = { y e. X | -. y R b } )
50 49 cbvmptv 
 |-  ( x e. X |-> { y e. X | -. y R x } ) = ( b e. X |-> { y e. X | -. y R b } )
51 ineq2 
 |-  ( w = { y e. X | -. y R b } -> ( z i^i w ) = ( z i^i { y e. X | -. y R b } ) )
52 51 eleq1d 
 |-  ( w = { y e. X | -. y R b } -> ( ( z i^i w ) e. A <-> ( z i^i { y e. X | -. y R b } ) e. A ) )
53 50 52 ralrnmptw 
 |-  ( A. b e. X { y e. X | -. y R b } e. _V -> ( A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A <-> A. b e. X ( z i^i { y e. X | -. y R b } ) e. A ) )
54 46 53 syl 
 |-  ( R e. TosetRel -> ( A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A <-> A. b e. X ( z i^i { y e. X | -. y R b } ) e. A ) )
55 54 ralbidv 
 |-  ( R e. TosetRel -> ( A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A <-> A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. b e. X ( z i^i { y e. X | -. y R b } ) e. A ) )
56 43 55 mpbird 
 |-  ( R e. TosetRel -> A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A )
57 2 raleqi 
 |-  ( A. w e. A ( z i^i w ) e. A <-> A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A )
58 2 57 raleqbii 
 |-  ( A. z e. A A. w e. A ( z i^i w ) e. A <-> A. z e. ran ( x e. X |-> { y e. X | -. y R x } ) A. w e. ran ( x e. X |-> { y e. X | -. y R x } ) ( z i^i w ) e. A )
59 56 58 sylibr 
 |-  ( R e. TosetRel -> A. z e. A A. w e. A ( z i^i w ) e. A )
60 15 pwexd 
 |-  ( R e. TosetRel -> ~P X e. _V )
61 ssrab2 
 |-  { y e. X | -. y R x } C_ X
62 15 adantr 
 |-  ( ( R e. TosetRel /\ x e. X ) -> X e. _V )
63 elpw2g 
 |-  ( X e. _V -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) )
64 62 63 syl 
 |-  ( ( R e. TosetRel /\ x e. X ) -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) )
65 61 64 mpbiri 
 |-  ( ( R e. TosetRel /\ x e. X ) -> { y e. X | -. y R x } e. ~P X )
66 65 fmpttd 
 |-  ( R e. TosetRel -> ( x e. X |-> { y e. X | -. y R x } ) : X --> ~P X )
67 66 frnd 
 |-  ( R e. TosetRel -> ran ( x e. X |-> { y e. X | -. y R x } ) C_ ~P X )
68 2 67 eqsstrid 
 |-  ( R e. TosetRel -> A C_ ~P X )
69 60 68 ssexd 
 |-  ( R e. TosetRel -> A e. _V )
70 inficl 
 |-  ( A e. _V -> ( A. z e. A A. w e. A ( z i^i w ) e. A <-> ( fi ` A ) = A ) )
71 69 70 syl 
 |-  ( R e. TosetRel -> ( A. z e. A A. w e. A ( z i^i w ) e. A <-> ( fi ` A ) = A ) )
72 59 71 mpbid 
 |-  ( R e. TosetRel -> ( fi ` A ) = A )