Metamath Proof Explorer

Theorem ordtbas2

Description: Lemma for ordtbas . (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 } )
ordtval.3 
|- B = ran ( x e. X |-> { y e. X | -. x R y } )
ordtval.4 
|- C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )
Assertion ordtbas2 
|- ( R e. TosetRel -> ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C ) )

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 ordtval.3 
 |-  B = ran ( x e. X |-> { y e. X | -. x R y } )
4 ordtval.4 
 |-  C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )
5 ssun1 
 |-  A C_ ( A u. B )
6 ssun2 
 |-  ( A u. B ) C_ ( { X } u. ( A u. B ) )
7 1 2 3 ordtuni 
 |-  ( R e. TosetRel -> X = U. ( { X } u. ( A u. B ) ) )
8 dmexg 
 |-  ( R e. TosetRel -> dom R e. _V )
9 1 8 eqeltrid 
 |-  ( R e. TosetRel -> X e. _V )
10 7 9 eqeltrrd 
 |-  ( R e. TosetRel -> U. ( { X } u. ( A u. B ) ) e. _V )
11 uniexb 
 |-  ( ( { X } u. ( A u. B ) ) e. _V <-> U. ( { X } u. ( A u. B ) ) e. _V )
12 10 11 sylibr 
 |-  ( R e. TosetRel -> ( { X } u. ( A u. B ) ) e. _V )
13 ssexg 
 |-  ( ( ( A u. B ) C_ ( { X } u. ( A u. B ) ) /\ ( { X } u. ( A u. B ) ) e. _V ) -> ( A u. B ) e. _V )
14 6 12 13 sylancr 
 |-  ( R e. TosetRel -> ( A u. B ) e. _V )
15 ssexg 
 |-  ( ( A C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> A e. _V )
16 5 14 15 sylancr 
 |-  ( R e. TosetRel -> A e. _V )
17 ssun2 
 |-  B C_ ( A u. B )
18 ssexg 
 |-  ( ( B C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> B e. _V )
19 17 14 18 sylancr 
 |-  ( R e. TosetRel -> B e. _V )
20 elfiun 
 |-  ( ( A e. _V /\ B e. _V ) -> ( z e. ( fi ` ( A u. B ) ) <-> ( z e. ( fi ` A ) \/ z e. ( fi ` B ) \/ E. m e. ( fi ` A ) E. n e. ( fi ` B ) z = ( m i^i n ) ) ) )
21 16 19 20 syl2anc 
 |-  ( R e. TosetRel -> ( z e. ( fi ` ( A u. B ) ) <-> ( z e. ( fi ` A ) \/ z e. ( fi ` B ) \/ E. m e. ( fi ` A ) E. n e. ( fi ` B ) z = ( m i^i n ) ) ) )
22 1 2 ordtbaslem 
 |-  ( R e. TosetRel -> ( fi ` A ) = A )
23 22 5 eqsstrdi 
 |-  ( R e. TosetRel -> ( fi ` A ) C_ ( A u. B ) )
24 ssun1 
 |-  ( A u. B ) C_ ( ( A u. B ) u. C )
25 23 24 sstrdi 
 |-  ( R e. TosetRel -> ( fi ` A ) C_ ( ( A u. B ) u. C ) )
26 25 sseld 
 |-  ( R e. TosetRel -> ( z e. ( fi ` A ) -> z e. ( ( A u. B ) u. C ) ) )
27 cnvtsr 
 |-  ( R e. TosetRel -> `' R e. TosetRel )
28 df-rn 
 |-  ran R = dom `' R
29 eqid 
 |-  ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } )
30 28 29 ordtbaslem 
 |-  ( `' R e. TosetRel -> ( fi ` ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) ) = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) )
31 27 30 syl 
 |-  ( R e. TosetRel -> ( fi ` ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) ) = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) )
32 tsrps 
 |-  ( R e. TosetRel -> R e. PosetRel )
33 1 psrn 
 |-  ( R e. PosetRel -> X = ran R )
34 32 33 syl 
 |-  ( R e. TosetRel -> X = ran R )
35 vex 
 |-  y e. _V
36 vex 
 |-  x e. _V
37 35 36 brcnv 
 |-  ( y `' R x <-> x R y )
38 37 bicomi 
 |-  ( x R y <-> y `' R x )
39 38 notbii 
 |-  ( -. x R y <-> -. y `' R x )
40 39 a1i 
 |-  ( R e. TosetRel -> ( -. x R y <-> -. y `' R x ) )
41 34 40 rabeqbidv 
 |-  ( R e. TosetRel -> { y e. X | -. x R y } = { y e. ran R | -. y `' R x } )
42 34 41 mpteq12dv 
 |-  ( R e. TosetRel -> ( x e. X |-> { y e. X | -. x R y } ) = ( x e. ran R |-> { y e. ran R | -. y `' R x } ) )
43 42 rneqd 
 |-  ( R e. TosetRel -> ran ( x e. X |-> { y e. X | -. x R y } ) = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) )
44 3 43 syl5eq 
 |-  ( R e. TosetRel -> B = ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) )
45 44 fveq2d 
 |-  ( R e. TosetRel -> ( fi ` B ) = ( fi ` ran ( x e. ran R |-> { y e. ran R | -. y `' R x } ) ) )
46 31 45 44 3eqtr4d 
 |-  ( R e. TosetRel -> ( fi ` B ) = B )
47 46 17 eqsstrdi 
 |-  ( R e. TosetRel -> ( fi ` B ) C_ ( A u. B ) )
48 47 24 sstrdi 
 |-  ( R e. TosetRel -> ( fi ` B ) C_ ( ( A u. B ) u. C ) )
49 48 sseld 
 |-  ( R e. TosetRel -> ( z e. ( fi ` B ) -> z e. ( ( A u. B ) u. C ) ) )
50 ssun2 
 |-  C C_ ( ( A u. B ) u. C )
51 22 2 eqtrdi 
 |-  ( R e. TosetRel -> ( fi ` A ) = ran ( x e. X |-> { y e. X | -. y R x } ) )
52 51 eleq2d 
 |-  ( R e. TosetRel -> ( m e. ( fi ` A ) <-> m e. ran ( x e. X |-> { y e. X | -. y R x } ) ) )
53 breq2 
 |-  ( x = a -> ( y R x <-> y R a ) )
54 53 notbid 
 |-  ( x = a -> ( -. y R x <-> -. y R a ) )
55 54 rabbidv 
 |-  ( x = a -> { y e. X | -. y R x } = { y e. X | -. y R a } )
56 55 cbvmptv 
 |-  ( x e. X |-> { y e. X | -. y R x } ) = ( a e. X |-> { y e. X | -. y R a } )
57 56 elrnmpt 
 |-  ( m e. _V -> ( m e. ran ( x e. X |-> { y e. X | -. y R x } ) <-> E. a e. X m = { y e. X | -. y R a } ) )
58 57 elv 
 |-  ( m e. ran ( x e. X |-> { y e. X | -. y R x } ) <-> E. a e. X m = { y e. X | -. y R a } )
59 52 58 bitrdi 
 |-  ( R e. TosetRel -> ( m e. ( fi ` A ) <-> E. a e. X m = { y e. X | -. y R a } ) )
60 46 3 eqtrdi 
 |-  ( R e. TosetRel -> ( fi ` B ) = ran ( x e. X |-> { y e. X | -. x R y } ) )
61 60 eleq2d 
 |-  ( R e. TosetRel -> ( n e. ( fi ` B ) <-> n e. ran ( x e. X |-> { y e. X | -. x R y } ) ) )
62 breq1 
 |-  ( x = b -> ( x R y <-> b R y ) )
63 62 notbid 
 |-  ( x = b -> ( -. x R y <-> -. b R y ) )
64 63 rabbidv 
 |-  ( x = b -> { y e. X | -. x R y } = { y e. X | -. b R y } )
65 64 cbvmptv 
 |-  ( x e. X |-> { y e. X | -. x R y } ) = ( b e. X |-> { y e. X | -. b R y } )
66 65 elrnmpt 
 |-  ( n e. _V -> ( n e. ran ( x e. X |-> { y e. X | -. x R y } ) <-> E. b e. X n = { y e. X | -. b R y } ) )
67 66 elv 
 |-  ( n e. ran ( x e. X |-> { y e. X | -. x R y } ) <-> E. b e. X n = { y e. X | -. b R y } )
68 61 67 bitrdi 
 |-  ( R e. TosetRel -> ( n e. ( fi ` B ) <-> E. b e. X n = { y e. X | -. b R y } ) )
69 59 68 anbi12d 
 |-  ( R e. TosetRel -> ( ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) <-> ( E. a e. X m = { y e. X | -. y R a } /\ E. b e. X n = { y e. X | -. b R y } ) ) )
70 reeanv 
 |-  ( E. a e. X E. b e. X ( m = { y e. X | -. y R a } /\ n = { y e. X | -. b R y } ) <-> ( E. a e. X m = { y e. X | -. y R a } /\ E. b e. X n = { y e. X | -. b R y } ) )
71 ineq12 
 |-  ( ( m = { y e. X | -. y R a } /\ n = { y e. X | -. b R y } ) -> ( m i^i n ) = ( { y e. X | -. y R a } i^i { y e. X | -. b R y } ) )
72 inrab 
 |-  ( { y e. X | -. y R a } i^i { y e. X | -. b R y } ) = { y e. X | ( -. y R a /\ -. b R y ) }
73 71 72 eqtrdi 
 |-  ( ( m = { y e. X | -. y R a } /\ n = { y e. X | -. b R y } ) -> ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
74 73 reximi 
 |-  ( E. b e. X ( m = { y e. X | -. y R a } /\ n = { y e. X | -. b R y } ) -> E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
75 74 reximi 
 |-  ( E. a e. X E. b e. X ( m = { y e. X | -. y R a } /\ n = { y e. X | -. b R y } ) -> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
76 70 75 sylbir 
 |-  ( ( E. a e. X m = { y e. X | -. y R a } /\ E. b e. X n = { y e. X | -. b R y } ) -> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
77 69 76 syl6bi 
 |-  ( R e. TosetRel -> ( ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) -> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } ) )
78 77 imp 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) ) -> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
79 vex 
 |-  m e. _V
80 79 inex1 
 |-  ( m i^i n ) e. _V
81 eqid 
 |-  ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) = ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )
82 81 elrnmpog 
 |-  ( ( m i^i n ) e. _V -> ( ( m i^i n ) e. ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) <-> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } ) )
83 80 82 ax-mp 
 |-  ( ( m i^i n ) e. ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) <-> E. a e. X E. b e. X ( m i^i n ) = { y e. X | ( -. y R a /\ -. b R y ) } )
84 78 83 sylibr 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) ) -> ( m i^i n ) e. ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) )
85 84 4 eleqtrrdi 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) ) -> ( m i^i n ) e. C )
86 50 85 sseldi 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) ) -> ( m i^i n ) e. ( ( A u. B ) u. C ) )
87 eleq1 
 |-  ( z = ( m i^i n ) -> ( z e. ( ( A u. B ) u. C ) <-> ( m i^i n ) e. ( ( A u. B ) u. C ) ) )
88 86 87 syl5ibrcom 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` A ) /\ n e. ( fi ` B ) ) ) -> ( z = ( m i^i n ) -> z e. ( ( A u. B ) u. C ) ) )
89 88 rexlimdvva 
 |-  ( R e. TosetRel -> ( E. m e. ( fi ` A ) E. n e. ( fi ` B ) z = ( m i^i n ) -> z e. ( ( A u. B ) u. C ) ) )
90 26 49 89 3jaod 
 |-  ( R e. TosetRel -> ( ( z e. ( fi ` A ) \/ z e. ( fi ` B ) \/ E. m e. ( fi ` A ) E. n e. ( fi ` B ) z = ( m i^i n ) ) -> z e. ( ( A u. B ) u. C ) ) )
91 21 90 sylbid 
 |-  ( R e. TosetRel -> ( z e. ( fi ` ( A u. B ) ) -> z e. ( ( A u. B ) u. C ) ) )
92 91 ssrdv 
 |-  ( R e. TosetRel -> ( fi ` ( A u. B ) ) C_ ( ( A u. B ) u. C ) )
93 ssfii 
 |-  ( ( A u. B ) e. _V -> ( A u. B ) C_ ( fi ` ( A u. B ) ) )
94 14 93 syl 
 |-  ( R e. TosetRel -> ( A u. B ) C_ ( fi ` ( A u. B ) ) )
95 94 adantr 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> ( A u. B ) C_ ( fi ` ( A u. B ) ) )
96 simprl 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> a e. X )
97 eqidd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R a } = { y e. X | -. y R a } )
98 55 rspceeqv 
 |-  ( ( a e. X /\ { y e. X | -. y R a } = { y e. X | -. y R a } ) -> E. x e. X { y e. X | -. y R a } = { y e. X | -. y R x } )
99 96 97 98 syl2anc 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> E. x e. X { y e. X | -. y R a } = { y e. X | -. y R x } )
100 9 adantr 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> X e. _V )
101 rabexg 
 |-  ( X e. _V -> { y e. X | -. y R a } e. _V )
102 eqid 
 |-  ( x e. X |-> { y e. X | -. y R x } ) = ( x e. X |-> { y e. X | -. y R x } )
103 102 elrnmpt 
 |-  ( { y e. X | -. y R a } e. _V -> ( { y e. X | -. y R a } e. ran ( x e. X |-> { y e. X | -. y R x } ) <-> E. x e. X { y e. X | -. y R a } = { y e. X | -. y R x } ) )
104 100 101 103 3syl 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> ( { y e. X | -. y R a } e. ran ( x e. X |-> { y e. X | -. y R x } ) <-> E. x e. X { y e. X | -. y R a } = { y e. X | -. y R x } ) )
105 99 104 mpbird 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R a } e. ran ( x e. X |-> { y e. X | -. y R x } ) )
106 105 2 eleqtrrdi 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R a } e. A )
107 5 106 sseldi 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R a } e. ( A u. B ) )
108 95 107 sseldd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. y R a } e. ( fi ` ( A u. B ) ) )
109 simprr 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> b e. X )
110 eqidd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. b R y } = { y e. X | -. b R y } )
111 64 rspceeqv 
 |-  ( ( b e. X /\ { y e. X | -. b R y } = { y e. X | -. b R y } ) -> E. x e. X { y e. X | -. b R y } = { y e. X | -. x R y } )
112 109 110 111 syl2anc 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> E. x e. X { y e. X | -. b R y } = { y e. X | -. x R y } )
113 rabexg 
 |-  ( X e. _V -> { y e. X | -. b R y } e. _V )
114 eqid 
 |-  ( x e. X |-> { y e. X | -. x R y } ) = ( x e. X |-> { y e. X | -. x R y } )
115 114 elrnmpt 
 |-  ( { y e. X | -. b R y } e. _V -> ( { y e. X | -. b R y } e. ran ( x e. X |-> { y e. X | -. x R y } ) <-> E. x e. X { y e. X | -. b R y } = { y e. X | -. x R y } ) )
116 100 113 115 3syl 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> ( { y e. X | -. b R y } e. ran ( x e. X |-> { y e. X | -. x R y } ) <-> E. x e. X { y e. X | -. b R y } = { y e. X | -. x R y } ) )
117 112 116 mpbird 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. b R y } e. ran ( x e. X |-> { y e. X | -. x R y } ) )
118 117 3 eleqtrrdi 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. b R y } e. B )
119 17 118 sseldi 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. b R y } e. ( A u. B ) )
120 95 119 sseldd 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | -. b R y } e. ( fi ` ( A u. B ) ) )
121 fiin 
 |-  ( ( { y e. X | -. y R a } e. ( fi ` ( A u. B ) ) /\ { y e. X | -. b R y } e. ( fi ` ( A u. B ) ) ) -> ( { y e. X | -. y R a } i^i { y e. X | -. b R y } ) e. ( fi ` ( A u. B ) ) )
122 108 120 121 syl2anc 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> ( { y e. X | -. y R a } i^i { y e. X | -. b R y } ) e. ( fi ` ( A u. B ) ) )
123 72 122 eqeltrrid 
 |-  ( ( R e. TosetRel /\ ( a e. X /\ b e. X ) ) -> { y e. X | ( -. y R a /\ -. b R y ) } e. ( fi ` ( A u. B ) ) )
124 123 ralrimivva 
 |-  ( R e. TosetRel -> A. a e. X A. b e. X { y e. X | ( -. y R a /\ -. b R y ) } e. ( fi ` ( A u. B ) ) )
125 81 fmpo 
 |-  ( A. a e. X A. b e. X { y e. X | ( -. y R a /\ -. b R y ) } e. ( fi ` ( A u. B ) ) <-> ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) : ( X X. X ) --> ( fi ` ( A u. B ) ) )
126 124 125 sylib 
 |-  ( R e. TosetRel -> ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) : ( X X. X ) --> ( fi ` ( A u. B ) ) )
127 126 frnd 
 |-  ( R e. TosetRel -> ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } ) C_ ( fi ` ( A u. B ) ) )
128 4 127 eqsstrid 
 |-  ( R e. TosetRel -> C C_ ( fi ` ( A u. B ) ) )
129 94 128 unssd 
 |-  ( R e. TosetRel -> ( ( A u. B ) u. C ) C_ ( fi ` ( A u. B ) ) )
130 92 129 eqssd 
 |-  ( R e. TosetRel -> ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C ) )