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 x A X 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 _ x v / x X
4 3 nfel1 x v / x X B
5 csbeq1a x = v X = v / x X
6 5 eleq1d x = v X B v / x X B
7 4 6 rspc v A x A X B v / x X B
8 7 impcom x A X B v A v / x X B
9 poirr R Po B v / x X B ¬ v / x X R v / x X
10 df-br v S v v v S
11 1 eleq2i v v S v v x y | X R Y
12 nfcv _ x R
13 nfcv _ x Y
14 3 12 13 nfbr x v / x X R Y
15 nfv y v / x X R v / x X
16 vex v V
17 5 breq1d x = v X R Y v / x X R Y
18 vex y 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 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 B ¬ v S v
26 8 25 sylan2 R Po B x A X B v A ¬ v S v
27 26 anassrs R Po B x A X B v A ¬ v S v
28 7 com12 x A X B v A v / x X B
29 nfcsb1v _ x w / x X
30 29 nfel1 x w / x X B
31 csbeq1a x = w X = w / x X
32 31 eleq1d x = w X B w / x X B
33 30 32 rspc w A x A X B w / x X B
34 33 com12 x A X B w A w / x X B
35 nfcsb1v _ x z / x X
36 35 nfel1 x z / x X B
37 csbeq1a x = z X = z / x X
38 37 eleq1d x = z X B z / x X B
39 36 38 rspc z A x A X B z / x X B
40 39 com12 x A X B z A z / x X B
41 28 34 40 3anim123d x A X B v A w A z A v / x X B w / x X B z / x X B
42 41 imp x A X B v A w A z A v / x X B w / x X B z / x X B
43 42 adantll R Po B x A X B v A w A z A v / x X B w / x X B z / x X B
44 potr R Po B v / x X B w / x X B z / x X 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 S
46 1 eleq2i v w S v w x y | X R Y
47 nfv y v / x X R w / x X
48 vex w 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 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 S
55 1 eleq2i w z S w z x y | X R Y
56 29 12 13 nfbr x w / x X R Y
57 nfv y w / x X R z / x X
58 vex z 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 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 S
67 1 eleq2i v z S v z x y | X R Y
68 nfv 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 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 B w / x X B z / x X B v S w w S z v S z
73 72 adantlr R Po B x A X B v / x X B w / x X B z / x X B v S w w S z v S z
74 43 73 syldan R Po B x A X B v A w A z A v S w w S z v S z
75 27 74 ispod R Po B x A X B S Po A