Metamath Proof Explorer

Theorem ordtrest2lem

Description: Lemma for ordtrest2 . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrest2.1 
|- X = dom R
ordtrest2.2 
|- ( ph -> R e. TosetRel )
ordtrest2.3 
|- ( ph -> A C_ X )
ordtrest2.4 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )
Assertion ordtrest2lem 
|- ( ph -> A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtrest2.1 
 |-  X = dom R
2 ordtrest2.2 
 |-  ( ph -> R e. TosetRel )
3 ordtrest2.3 
 |-  ( ph -> A C_ X )
4 ordtrest2.4 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )
5 inrab2 
 |-  ( { w e. X | -. w R z } i^i A ) = { w e. ( X i^i A ) | -. w R z }
6 sseqin2 
 |-  ( A C_ X <-> ( X i^i A ) = A )
7 3 6 sylib 
 |-  ( ph -> ( X i^i A ) = A )
8 7 adantr 
 |-  ( ( ph /\ z e. X ) -> ( X i^i A ) = A )
9 8 rabeqdv 
 |-  ( ( ph /\ z e. X ) -> { w e. ( X i^i A ) | -. w R z } = { w e. A | -. w R z } )
10 5 9 eqtrid 
 |-  ( ( ph /\ z e. X ) -> ( { w e. X | -. w R z } i^i A ) = { w e. A | -. w R z } )
11 inex1g 
 |-  ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. _V )
12 2 11 syl 
 |-  ( ph -> ( R i^i ( A X. A ) ) e. _V )
13 eqid 
 |-  dom ( R i^i ( A X. A ) ) = dom ( R i^i ( A X. A ) )
14 13 ordttopon 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` dom ( R i^i ( A X. A ) ) ) )
15 12 14 syl 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` dom ( R i^i ( A X. A ) ) ) )
16 tsrps 
 |-  ( R e. TosetRel -> R e. PosetRel )
17 2 16 syl 
 |-  ( ph -> R e. PosetRel )
18 1 psssdm 
 |-  ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )
19 17 3 18 syl2anc 
 |-  ( ph -> dom ( R i^i ( A X. A ) ) = A )
20 19 fveq2d 
 |-  ( ph -> ( TopOn ` dom ( R i^i ( A X. A ) ) ) = ( TopOn ` A ) )
21 15 20 eleqtrd 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` A ) )
22 toponmax 
 |-  ( ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` A ) -> A e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
23 21 22 syl 
 |-  ( ph -> A e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
24 23 adantr 
 |-  ( ( ph /\ z e. X ) -> A e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
25 rabid2 
 |-  ( A = { w e. A | -. w R z } <-> A. w e. A -. w R z )
26 eleq1 
 |-  ( A = { w e. A | -. w R z } -> ( A e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
27 25 26 sylbir 
 |-  ( A. w e. A -. w R z -> ( A e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
28 24 27 syl5ibcom 
 |-  ( ( ph /\ z e. X ) -> ( A. w e. A -. w R z -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
29 dfrex2 
 |-  ( E. w e. A w R z <-> -. A. w e. A -. w R z )
30 breq1 
 |-  ( w = x -> ( w R z <-> x R z ) )
31 30 cbvrexvw 
 |-  ( E. w e. A w R z <-> E. x e. A x R z )
32 29 31 bitr3i 
 |-  ( -. A. w e. A -. w R z <-> E. x e. A x R z )
33 ordttop 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top )
34 12 33 syl 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top )
35 34 adantr 
 |-  ( ( ph /\ z e. X ) -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top )
36 0opn 
 |-  ( ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top -> (/) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
37 35 36 syl 
 |-  ( ( ph /\ z e. X ) -> (/) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
38 37 adantr 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> (/) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
39 eleq1 
 |-  ( { w e. A | -. w R z } = (/) -> ( { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> (/) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
40 38 39 syl5ibrcom 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> ( { w e. A | -. w R z } = (/) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
41 rabn0 
 |-  ( { w e. A | -. w R z } =/= (/) <-> E. w e. A -. w R z )
42 breq1 
 |-  ( w = y -> ( w R z <-> y R z ) )
43 42 notbid 
 |-  ( w = y -> ( -. w R z <-> -. y R z ) )
44 43 cbvrexvw 
 |-  ( E. w e. A -. w R z <-> E. y e. A -. y R z )
45 41 44 bitri 
 |-  ( { w e. A | -. w R z } =/= (/) <-> E. y e. A -. y R z )
46 2 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> R e. TosetRel )
47 3 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> A C_ X )
48 47 sselda 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> y e. X )
49 simpllr 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> z e. X )
50 1 tsrlin 
 |-  ( ( R e. TosetRel /\ y e. X /\ z e. X ) -> ( y R z \/ z R y ) )
51 46 48 49 50 syl3anc 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> ( y R z \/ z R y ) )
52 51 ord 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> ( -. y R z -> z R y ) )
53 an4 
 |-  ( ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x R z /\ z R y ) ) )
54 rabss 
 |-  ( { z e. X | ( x R z /\ z R y ) } C_ A <-> A. z e. X ( ( x R z /\ z R y ) -> z e. A ) )
55 4 54 sylib 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> A. z e. X ( ( x R z /\ z R y ) -> z e. A ) )
56 55 r19.21bi 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ z e. X ) -> ( ( x R z /\ z R y ) -> z e. A ) )
57 56 an32s 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ y e. A ) ) -> ( ( x R z /\ z R y ) -> z e. A ) )
58 57 impr 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ y e. A ) /\ ( x R z /\ z R y ) ) ) -> z e. A )
59 53 58 sylan2b 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> z e. A )
60 brinxp 
 |-  ( ( w e. A /\ z e. A ) -> ( w R z <-> w ( R i^i ( A X. A ) ) z ) )
61 60 ancoms 
 |-  ( ( z e. A /\ w e. A ) -> ( w R z <-> w ( R i^i ( A X. A ) ) z ) )
62 61 notbid 
 |-  ( ( z e. A /\ w e. A ) -> ( -. w R z <-> -. w ( R i^i ( A X. A ) ) z ) )
63 62 rabbidva 
 |-  ( z e. A -> { w e. A | -. w R z } = { w e. A | -. w ( R i^i ( A X. A ) ) z } )
64 59 63 syl 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> { w e. A | -. w R z } = { w e. A | -. w ( R i^i ( A X. A ) ) z } )
65 19 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> dom ( R i^i ( A X. A ) ) = A )
66 65 rabeqdv 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> { w e. dom ( R i^i ( A X. A ) ) | -. w ( R i^i ( A X. A ) ) z } = { w e. A | -. w ( R i^i ( A X. A ) ) z } )
67 64 66 eqtr4d 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> { w e. A | -. w R z } = { w e. dom ( R i^i ( A X. A ) ) | -. w ( R i^i ( A X. A ) ) z } )
68 12 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> ( R i^i ( A X. A ) ) e. _V )
69 59 65 eleqtrrd 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> z e. dom ( R i^i ( A X. A ) ) )
70 13 ordtopn1 
 |-  ( ( ( R i^i ( A X. A ) ) e. _V /\ z e. dom ( R i^i ( A X. A ) ) ) -> { w e. dom ( R i^i ( A X. A ) ) | -. w ( R i^i ( A X. A ) ) z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
71 68 69 70 syl2anc 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> { w e. dom ( R i^i ( A X. A ) ) | -. w ( R i^i ( A X. A ) ) z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
72 67 71 eqeltrd 
 |-  ( ( ( ph /\ z e. X ) /\ ( ( x e. A /\ x R z ) /\ ( y e. A /\ z R y ) ) ) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
73 72 anassrs 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ ( y e. A /\ z R y ) ) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
74 73 expr 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> ( z R y -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
75 52 74 syld 
 |-  ( ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) /\ y e. A ) -> ( -. y R z -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
76 75 rexlimdva 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> ( E. y e. A -. y R z -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
77 45 76 syl5bi 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> ( { w e. A | -. w R z } =/= (/) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
78 40 77 pm2.61dne 
 |-  ( ( ( ph /\ z e. X ) /\ ( x e. A /\ x R z ) ) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
79 78 rexlimdvaa 
 |-  ( ( ph /\ z e. X ) -> ( E. x e. A x R z -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
80 32 79 syl5bi 
 |-  ( ( ph /\ z e. X ) -> ( -. A. w e. A -. w R z -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
81 28 80 pm2.61d 
 |-  ( ( ph /\ z e. X ) -> { w e. A | -. w R z } e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
82 10 81 eqeltrd 
 |-  ( ( ph /\ z e. X ) -> ( { w e. X | -. w R z } i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
83 82 ralrimiva 
 |-  ( ph -> A. z e. X ( { w e. X | -. w R z } i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
84 2 dmexd 
 |-  ( ph -> dom R e. _V )
85 1 84 eqeltrid 
 |-  ( ph -> X e. _V )
86 rabexg 
 |-  ( X e. _V -> { w e. X | -. w R z } e. _V )
87 85 86 syl 
 |-  ( ph -> { w e. X | -. w R z } e. _V )
88 87 ralrimivw 
 |-  ( ph -> A. z e. X { w e. X | -. w R z } e. _V )
89 eqid 
 |-  ( z e. X |-> { w e. X | -. w R z } ) = ( z e. X |-> { w e. X | -. w R z } )
90 ineq1 
 |-  ( v = { w e. X | -. w R z } -> ( v i^i A ) = ( { w e. X | -. w R z } i^i A ) )
91 90 eleq1d 
 |-  ( v = { w e. X | -. w R z } -> ( ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( { w e. X | -. w R z } i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
92 89 91 ralrnmptw 
 |-  ( A. z e. X { w e. X | -. w R z } e. _V -> ( A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> A. z e. X ( { w e. X | -. w R z } i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
93 88 92 syl 
 |-  ( ph -> ( A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> A. z e. X ( { w e. X | -. w R z } i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
94 83 93 mpbird 
 |-  ( ph -> A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )