Theorem pofun 4040

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

Hypotheses

Ref	Expression
pofun.1	|- S = { <.x , y >. | X R Y }
pofun.2	|- (x = y -> X = Y)

Assertion

Ref	Expression
pofun	|- (( R Po B /\ A.x e. A X e. B) -> S Po A)

Distinct variable groups:   x, R,y   y, X   x, Y   x,A   x,B

Allowed substitution hints:   A(y)   B(y)   S(x,y)   X(x)   Y(y)

Proof of Theorem pofun

Dummy variables v w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcsb1v 2876	. . . . . . 7 |- F/_x [_v / x ]_ X
2	1	nfel1 2185	. . . . . 6 |- F/x [_v / x ]_ X e. B
3		csbeq1a 2854	. . . . . . 7 |- (x = v -> X = [_v / x ]_ X)
4	3	eleq1d 2103	. . . . . 6 |- (x = v -> ( X e. B <-> [_v / x ]_ X e. B))
5	2, 4	rspc 2644	. . . . 5 |- (v e. A -> (A.x e. A X e. B -> [_v / x ]_ X e. B))
6	5	impcom 116	. . . 4 |- ((A.x e. A X e. B /\ v e. A) -> [_v / x ]_ X e. B)
7		poirr 4035	. . . . 5 |- (( R Po B /\ [_v / x ]_ X e. B) -> -. [_v / x ]_ X R [_v / x ]_ X)
8		df-br 3756	. . . . . 6 |- (v Sv <-> <.v , v >. e. S)
9		pofun.1	. . . . . . 7 |- S = { <.x , y >. | X R Y }
10	9	eleq2i 2101	. . . . . 6 |- ( <.v , v >. e. S <-> <.v , v >. e. { <.x , y >. | X R Y })
11		nfcv 2175	. . . . . . . 8 |- F/_x R
12		nfcv 2175	. . . . . . . 8 |- F/_x Y
13	1, 11, 12	nfbr 3799	. . . . . . 7 |- F/x [_v / x ]_ X R Y
14		nfv 1418	. . . . . . 7 |- F/y [_v / x ]_ X R [_v / x ]_ X
15		vex 2554	. . . . . . 7 |- v e. _V
16	3	breq1d 3765	. . . . . . 7 |- (x = v -> ( X R Y <-> [_v / x ]_ X R Y))
17		vex 2554	. . . . . . . . . 10 |- y e. _V
18		pofun.2	. . . . . . . . . 10 |- (x = y -> X = Y)
19	17, 12, 18	csbief 2885	. . . . . . . . 9 |- [_y / x ]_ X = Y
20		csbeq1 2849	. . . . . . . . 9 |- (y = v -> [_y / x ]_ X = [_v / x ]_ X)
21	19, 20	syl5eqr 2083	. . . . . . . 8 |- (y = v -> Y = [_v / x ]_ X)
22	21	breq2d 3767	. . . . . . 7 |- (y = v -> ( [_v / x ]_ X R Y <-> [_v / x ]_ X R [_v / x ]_ X))
23	13, 14, 15, 15, 16, 22	opelopabf 4002	. . . . . 6 |- ( <.v , v >. e. { <.x , y >. | X R Y } <-> [_v / x ]_ X R [_v / x ]_ X)
24	8, 10, 23	3bitri 195	. . . . 5 |- (v Sv <-> [_v / x ]_ X R [_v / x ]_ X)
25	7, 24	sylnibr 601	. . . 4 |- (( R Po B /\ [_v / x ]_ X e. B) -> -. v Sv)
26	6, 25	sylan2 270	. . 3 |- (( R Po B /\ (A.x e. A X e. B /\ v e. A)) -> -. v Sv)
27	26	anassrs 380	. 2 |- ((( R Po B /\ A.x e. A X e. B) /\ v e. A) -> -. v Sv)
28	5	com12 27	. . . . . 6 |- (A.x e. A X e. B -> (v e. A -> [_v / x ]_ X e. B))
29		nfcsb1v 2876	. . . . . . . . 9 |- F/_x [_w / x ]_ X
30	29	nfel1 2185	. . . . . . . 8 |- F/x [_w / x ]_ X e. B
31		csbeq1a 2854	. . . . . . . . 9 |- (x = w -> X = [_w / x ]_ X)
32	31	eleq1d 2103	. . . . . . . 8 |- (x = w -> ( X e. B <-> [_w / x ]_ X e. B))
33	30, 32	rspc 2644	. . . . . . 7 |- (w e. A -> (A.x e. A X e. B -> [_w / x ]_ X e. B))
34	33	com12 27	. . . . . 6 |- (A.x e. A X e. B -> (w e. A -> [_w / x ]_ X e. B))
35		nfcsb1v 2876	. . . . . . . . 9 |- F/_x [_z / x ]_ X
36	35	nfel1 2185	. . . . . . . 8 |- F/x [_z / x ]_ X e. B
37		csbeq1a 2854	. . . . . . . . 9 |- (x = z -> X = [_z / x ]_ X)
38	37	eleq1d 2103	. . . . . . . 8 |- (x = z -> ( X e. B <-> [_z / x ]_ X e. B))
39	36, 38	rspc 2644	. . . . . . 7 |- (z e. A -> (A.x e. A X e. B -> [_z / x ]_ X e. B))
40	39	com12 27	. . . . . 6 |- (A.x e. A X e. B -> (z e. A -> [_z / x ]_ X e. B))
41	28, 34, 40	3anim123d 1213	. . . . 5 |- (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 115	. . . 4 |- ((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 445	. . 3 |- ((( 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 4036	. . . . 5 |- (( 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 3756	. . . . . . 7 |- (v Sw <-> <.v , w >. e. S)
46	9	eleq2i 2101	. . . . . . 7 |- ( <.v , w >. e. S <-> <.v , w >. e. { <.x , y >. | X R Y })
47		nfv 1418	. . . . . . . 8 |- F/y [_v / x ]_ X R [_w / x ]_ X
48		vex 2554	. . . . . . . 8 |- w e. _V
49		csbeq1 2849	. . . . . . . . . 10 |- (y = w -> [_y / x ]_ X = [_w / x ]_ X)
50	19, 49	syl5eqr 2083	. . . . . . . . 9 |- (y = w -> Y = [_w / x ]_ X)
51	50	breq2d 3767	. . . . . . . 8 |- (y = w -> ( [_v / x ]_ X R Y <-> [_v / x ]_ X R [_w / x ]_ X))
52	13, 47, 15, 48, 16, 51	opelopabf 4002	. . . . . . 7 |- ( <.v , w >. e. { <.x , y >. | X R Y } <-> [_v / x ]_ X R [_w / x ]_ X)
53	45, 46, 52	3bitri 195	. . . . . 6 |- (v Sw <-> [_v / x ]_ X R [_w / x ]_ X)
54		df-br 3756	. . . . . . 7 |- (w Sz <-> <.w , z >. e. S)
55	9	eleq2i 2101	. . . . . . 7 |- ( <.w , z >. e. S <-> <.w , z >. e. { <.x , y >. | X R Y })
56	29, 11, 12	nfbr 3799	. . . . . . . 8 |- F/x [_w / x ]_ X R Y
57		nfv 1418	. . . . . . . 8 |- F/y [_w / x ]_ X R [_z / x ]_ X
58		vex 2554	. . . . . . . 8 |- z e. _V
59	31	breq1d 3765	. . . . . . . 8 |- (x = w -> ( X R Y <-> [_w / x ]_ X R Y))
60		csbeq1 2849	. . . . . . . . . 10 |- (y = z -> [_y / x ]_ X = [_z / x ]_ X)
61	19, 60	syl5eqr 2083	. . . . . . . . 9 |- (y = z -> Y = [_z / x ]_ X)
62	61	breq2d 3767	. . . . . . . 8 |- (y = z -> ( [_w / x ]_ X R Y <-> [_w / x ]_ X R [_z / x ]_ X))
63	56, 57, 48, 58, 59, 62	opelopabf 4002	. . . . . . 7 |- ( <.w , z >. e. { <.x , y >. | X R Y } <-> [_w / x ]_ X R [_z / x ]_ X)
64	54, 55, 63	3bitri 195	. . . . . 6 |- (w Sz <-> [_w / x ]_ X R [_z / x ]_ X)
65	53, 64	anbi12i 433	. . . . 5 |- ((v Sw /\ w Sz) <-> ( [_v / x ]_ X R [_w / x ]_ X /\ [_w / x ]_ X R [_z / x ]_ X))
66		df-br 3756	. . . . . 6 |- (v Sz <-> <.v , z >. e. S)
67	9	eleq2i 2101	. . . . . 6 |- ( <.v , z >. e. S <-> <.v , z >. e. { <.x , y >. | X R Y })
68		nfv 1418	. . . . . . 7 |- F/y [_v / x ]_ X R [_z / x ]_ X
69	61	breq2d 3767	. . . . . . 7 |- (y = z -> ( [_v / x ]_ X R Y <-> [_v / x ]_ X R [_z / x ]_ X))
70	13, 68, 15, 58, 16, 69	opelopabf 4002	. . . . . 6 |- ( <.v , z >. e. { <.x , y >. | X R Y } <-> [_v / x ]_ X R [_z / x ]_ X)
71	66, 67, 70	3bitri 195	. . . . 5 |- (v Sz <-> [_v / x ]_ X R [_z / x ]_ X)
72	44, 65, 71	3imtr4g 194	. . . 4 |- (( R Po B /\ ( [_v / x ]_ X e. B /\ [_w / x ]_ X e. B /\ [_z / x ]_ X e. B)) -> ((v Sw /\ w Sz) -> v Sz))
73	72	adantlr 446	. . 3 |- ((( 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 Sw /\ w Sz) -> v Sz))
74	43, 73	syldan 266	. 2 |- ((( R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A /\ z e. A)) -> ((v Sw /\ w Sz) -> v Sz))
75	27, 74	ispod 4032	1 |- (( R Po B /\ A.x e. A X e. B) -> S Po A)

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   /\ w3a 884   = wceq 1242   e. wcel 1390  A.wral 2300   [_csb 2846   <.cop 3370   class class class wbr 3755   {copab 3808   Po wpo 4022

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-po 4024

This theorem is referenced by: (None)