Metamath Proof Explorer

Theorem pofun

Description: A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011)

Ref Expression
Hypotheses pofun.1 ${⊢}{S}=\left\{⟨{x},{y}⟩|{X}{R}{Y}\right\}$
pofun.2 ${⊢}{x}={y}\to {X}={Y}$
Assertion pofun ${⊢}\left({R}\mathrm{Po}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {B}\right)\to {S}\mathrm{Po}{A}$

Proof

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