Metamath Proof Explorer

Theorem pofun

Description: The inverse image of a partial order is a partial order. (Contributed by Jeff Madsen, 18-Jun-2011)

Ref Expression
Hypotheses pofun.1 
|- S = { <. x , y >. | X R Y }
pofun.2 
|- ( x = y -> X = Y )
Assertion pofun 
|- ( ( R Po B /\ A. x e. A X e. B ) -> S Po A )

Proof

Step Hyp Ref Expression
1 pofun.1 
 |-  S = { <. x , y >. | X R Y }
2 pofun.2 
 |-  ( x = y -> X = Y )
3 nfcsb1v 
 |-  F/_ x [_ v / x ]_ X
4 3 nfel1 
 |-  F/ x [_ v / x ]_ X e. B
5 csbeq1a 
 |-  ( x = v -> X = [_ v / x ]_ X )
6 5 eleq1d 
 |-  ( x = v -> ( X e. B <-> [_ v / x ]_ X e. B ) )
7 4 6 rspc 
 |-  ( v e. A -> ( A. x e. A X e. B -> [_ v / x ]_ X e. B ) )
8 7 impcom 
 |-  ( ( A. x e. A X e. B /\ v e. A ) -> [_ v / x ]_ X e. B )
9 poirr 
 |-  ( ( R Po B /\ [_ v / x ]_ X e. B ) -> -. [_ v / x ]_ X R [_ v / x ]_ X )
10 df-br 
 |-  ( v S v <-> <. v , v >. e. S )
11 1 eleq2i 
 |-  ( <. v , v >. e. S <-> <. v , v >. e. { <. x , y >. | X R Y } )
12 nfcv 
 |-  F/_ x R
13 nfcv 
 |-  F/_ x Y
14 3 12 13 nfbr 
 |-  F/ x [_ v / x ]_ X R Y
15 nfv 
 |-  F/ y [_ v / x ]_ X R [_ v / x ]_ X
16 vex 
 |-  v e. _V
17 5 breq1d 
 |-  ( x = v -> ( X R Y <-> [_ v / x ]_ X R Y ) )
18 vex 
 |-  y e. _V
19 18 2 csbie 
 |-  [_ y / x ]_ X = Y
20 csbeq1 
 |-  ( y = v -> [_ y / x ]_ X = [_ v / x ]_ X )
21 19 20 eqtr3id 
 |-  ( y = v -> Y = [_ v / x ]_ X )
22 21 breq2d 
 |-  ( y = v -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ v / x ]_ X ) )
23 14 15 16 16 17 22 opelopabf 
 |-  ( <. v , v >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ v / x ]_ X )
24 10 11 23 3bitri 
 |-  ( v S v <-> [_ v / x ]_ X R [_ v / x ]_ X )
25 9 24 sylnibr 
 |-  ( ( R Po B /\ [_ v / x ]_ X e. B ) -> -. v S v )
26 8 25 sylan2 
 |-  ( ( R Po B /\ ( A. x e. A X e. B /\ v e. A ) ) -> -. v S v )
27 26 anassrs 
 |-  ( ( ( R Po B /\ A. x e. A X e. B ) /\ v e. A ) -> -. v S v )
28 7 com12 
 |-  ( A. x e. A X e. B -> ( v e. A -> [_ v / x ]_ X e. B ) )
29 nfcsb1v 
 |-  F/_ x [_ w / x ]_ X
30 29 nfel1 
 |-  F/ x [_ w / x ]_ X e. B
31 csbeq1a 
 |-  ( x = w -> X = [_ w / x ]_ X )
32 31 eleq1d 
 |-  ( x = w -> ( X e. B <-> [_ w / x ]_ X e. B ) )
33 30 32 rspc 
 |-  ( w e. A -> ( A. x e. A X e. B -> [_ w / x ]_ X e. B ) )
34 33 com12 
 |-  ( A. x e. A X e. B -> ( w e. A -> [_ w / x ]_ X e. B ) )
35 nfcsb1v 
 |-  F/_ x [_ z / x ]_ X
36 35 nfel1 
 |-  F/ x [_ z / x ]_ X e. B
37 csbeq1a 
 |-  ( x = z -> X = [_ z / x ]_ X )
38 37 eleq1d 
 |-  ( x = z -> ( X e. B <-> [_ z / x ]_ X e. B ) )
39 36 38 rspc 
 |-  ( z e. A -> ( A. x e. A X e. B -> [_ z / x ]_ X e. B ) )
40 39 com12 
 |-  ( A. x e. A X e. B -> ( z e. A -> [_ z / x ]_ X e. B ) )
41 28 34 40 3anim123d 
 |-  ( A. x e. A X e. B -> ( ( v e. A /\ w e. A /\ z e. A ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) )
42 41 imp 
 |-  ( ( A. x e. A X e. B /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) )
43 42 adantll 
 |-  ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) )
44 potr 
 |-  ( ( R Po B /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( [_ v / x ]_ X R [_ w / x ]_ X /\ [_ w / x ]_ X R [_ z / x ]_ X ) -> [_ v / x ]_ X R [_ z / x ]_ X ) )
45 df-br 
 |-  ( v S w <-> <. v , w >. e. S )
46 1 eleq2i 
 |-  ( <. v , w >. e. S <-> <. v , w >. e. { <. x , y >. | X R Y } )
47 nfv 
 |-  F/ y [_ v / x ]_ X R [_ w / x ]_ X
48 vex 
 |-  w e. _V
49 csbeq1 
 |-  ( y = w -> [_ y / x ]_ X = [_ w / x ]_ X )
50 19 49 eqtr3id 
 |-  ( y = w -> Y = [_ w / x ]_ X )
51 50 breq2d 
 |-  ( y = w -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ w / x ]_ X ) )
52 14 47 16 48 17 51 opelopabf 
 |-  ( <. v , w >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ w / x ]_ X )
53 45 46 52 3bitri 
 |-  ( v S w <-> [_ v / x ]_ X R [_ w / x ]_ X )
54 df-br 
 |-  ( w S z <-> <. w , z >. e. S )
55 1 eleq2i 
 |-  ( <. w , z >. e. S <-> <. w , z >. e. { <. x , y >. | X R Y } )
56 29 12 13 nfbr 
 |-  F/ x [_ w / x ]_ X R Y
57 nfv 
 |-  F/ y [_ w / x ]_ X R [_ z / x ]_ X
58 vex 
 |-  z e. _V
59 31 breq1d 
 |-  ( x = w -> ( X R Y <-> [_ w / x ]_ X R Y ) )
60 csbeq1 
 |-  ( y = z -> [_ y / x ]_ X = [_ z / x ]_ X )
61 19 60 eqtr3id 
 |-  ( y = z -> Y = [_ z / x ]_ X )
62 61 breq2d 
 |-  ( y = z -> ( [_ w / x ]_ X R Y <-> [_ w / x ]_ X R [_ z / x ]_ X ) )
63 56 57 48 58 59 62 opelopabf 
 |-  ( <. w , z >. e. { <. x , y >. | X R Y } <-> [_ w / x ]_ X R [_ z / x ]_ X )
64 54 55 63 3bitri 
 |-  ( w S z <-> [_ w / x ]_ X R [_ z / x ]_ X )
65 53 64 anbi12i 
 |-  ( ( v S w /\ w S z ) <-> ( [_ v / x ]_ X R [_ w / x ]_ X /\ [_ w / x ]_ X R [_ z / x ]_ X ) )
66 df-br 
 |-  ( v S z <-> <. v , z >. e. S )
67 1 eleq2i 
 |-  ( <. v , z >. e. S <-> <. v , z >. e. { <. x , y >. | X R Y } )
68 nfv 
 |-  F/ y [_ v / x ]_ X R [_ z / x ]_ X
69 61 breq2d 
 |-  ( y = z -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ z / x ]_ X ) )
70 14 68 16 58 17 69 opelopabf 
 |-  ( <. v , z >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ z / x ]_ X )
71 66 67 70 3bitri 
 |-  ( v S z <-> [_ v / x ]_ X R [_ z / x ]_ X )
72 44 65 71 3imtr4g 
 |-  ( ( R Po B /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( v S w /\ w S z ) -> v S z ) )
73 72 adantlr 
 |-  ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( v S w /\ w S z ) -> v S z ) )
74 43 73 syldan 
 |-  ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( ( v S w /\ w S z ) -> v S z ) )
75 27 74 ispod 
 |-  ( ( R Po B /\ A. x e. A X e. B ) -> S Po A )