Theorem pofun 15772

Description: A function preserves a partial order relation.

Hypotheses

Ref	Expression
pofun.1	|- S = {<.x, y>. | XRY}
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

Proof of Theorem pofun

Step	Hyp	Ref	Expression
1		poirr 3597	. . . . . . . . . . 11 |- ((R Po B /\ [_v / x]_X e. B) -> -. [_v / x]_XR[_v / x]_X)
2		df-br 3339	. . . . . . . . . . . . 13 |- (vSv <-> <.v, v>. e. S)
3		pofun.1	. . . . . . . . . . . . . 14 |- S = {<.x, y>. | XRY}
4	3	eleq2i 1961	. . . . . . . . . . . . 13 |- (<.v, v>. e. S <-> <.v, v>. e. {<.x, y>. | XRY})
5		visset 2295	. . . . . . . . . . . . . . . 16 |- v e. _V
6		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (z e. v -> A.x z e. v)
7	5, 6	hbcsb1 2568	. . . . . . . . . . . . . . 15 |- (z e. [_v / x]_X -> A.x z e. [_v / x]_X)
8		ax-17 1317	. . . . . . . . . . . . . . 15 |- (z e. R -> A.x z e. R)
9		ax-17 1317	. . . . . . . . . . . . . . 15 |- (z e. Y -> A.x z e. Y)
10	7, 8, 9	hbbr 3381	. . . . . . . . . . . . . 14 |- ([_v / x]_XRY -> A.x[_v / x]_XRY)
11		ax-17 1317	. . . . . . . . . . . . . 14 |- ([_v / x]_XR[_v / x]_X -> A.y[_v / x]_XR[_v / x]_X)
12		csbeq1a 2546	. . . . . . . . . . . . . . 15 |- (x = v -> X = [_v / x]_X)
13	12	breq1d 3348	. . . . . . . . . . . . . 14 |- (x = v -> (XRY <-> [_v / x]_XRY))
14		csbeq1 2542	. . . . . . . . . . . . . . . 16 |- (y = v -> [_y / x]_X = [_v / x]_X)
15		visset 2295	. . . . . . . . . . . . . . . . 17 |- y e. _V
16		pofun.2	. . . . . . . . . . . . . . . . 17 |- (x = y -> X = Y)
17	15, 9, 16	csbief 2576	. . . . . . . . . . . . . . . 16 |- [_y / x]_X = Y
18	14, 17	syl5eqr 1942	. . . . . . . . . . . . . . 15 |- (y = v -> Y = [_v / x]_X)
19	18	breq2d 3350	. . . . . . . . . . . . . 14 |- (y = v -> ([_v / x]_XRY <-> [_v / x]_XR[_v / x]_X))
20	10, 11, 5, 5, 13, 19	opelopabf 3572	. . . . . . . . . . . . 13 |- (<.v, v>. e. {<.x, y>. | XRY} <-> [_v / x]_XR[_v / x]_X)
21	2, 4, 20	3bitri 194	. . . . . . . . . . . 12 |- (vSv <-> [_v / x]_XR[_v / x]_X)
22	21	notbii 204	. . . . . . . . . . 11 |- (-. vSv <-> -. [_v / x]_XR[_v / x]_X)
23	1, 22	sylibr 217	. . . . . . . . . 10 |- ((R Po B /\ [_v / x]_X e. B) -> -. vSv)
24		ax-17 1317	. . . . . . . . . . . . 13 |- (z e. B -> A.x z e. B)
25	7, 24	hbel 1996	. . . . . . . . . . . 12 |- ([_v / x]_X e. B -> A.x[_v / x]_X e. B)
26	12	eleq1d 1963	. . . . . . . . . . . 12 |- (x = v -> (X e. B <-> [_v / x]_X e. B))
27	25, 26	rcla4 2373	. . . . . . . . . . 11 |- (v e. A -> (A.x e. A X e. B -> [_v / x]_X e. B))
28	27	impcom 378	. . . . . . . . . 10 |- ((A.x e. A X e. B /\ v e. A) -> [_v / x]_X e. B)
29	23, 28	sylan2 500	. . . . . . . . 9 |- ((R Po B /\ (A.x e. A X e. B /\ v e. A)) -> -. vSv)
30	29	anassrs 489	. . . . . . . 8 |- (((R Po B /\ A.x e. A X e. B) /\ v e. A) -> -. vSv)
31	30	adantrr 431	. . . . . . 7 |- (((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A)) -> -. vSv)
32	31	adantr 425	. . . . . 6 |- ((((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A)) /\ z e. A) -> -. vSv)
33	27	com12 14	. . . . . . . . . . . 12 |- (A.x e. A X e. B -> (v e. A -> [_v / x]_X e. B))
34		visset 2295	. . . . . . . . . . . . . . . 16 |- w e. _V
35		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (z e. w -> A.x z e. w)
36	34, 35	hbcsb1 2568	. . . . . . . . . . . . . . 15 |- (z e. [_w / x]_X -> A.x z e. [_w / x]_X)
37	36, 24	hbel 1996	. . . . . . . . . . . . . 14 |- ([_w / x]_X e. B -> A.x[_w / x]_X e. B)
38		csbeq1a 2546	. . . . . . . . . . . . . . 15 |- (x = w -> X = [_w / x]_X)
39	38	eleq1d 1963	. . . . . . . . . . . . . 14 |- (x = w -> (X e. B <-> [_w / x]_X e. B))
40	37, 39	rcla4 2373	. . . . . . . . . . . . 13 |- (w e. A -> (A.x e. A X e. B -> [_w / x]_X e. B))
41	40	com12 14	. . . . . . . . . . . 12 |- (A.x e. A X e. B -> (w e. A -> [_w / x]_X e. B))
42		visset 2295	. . . . . . . . . . . . . . . 16 |- z e. _V
43		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (w e. z -> A.x w e. z)
44	42, 43	hbcsb1 2568	. . . . . . . . . . . . . . 15 |- (w e. [_z / x]_X -> A.x w e. [_z / x]_X)
45	44, 24	hbel 1996	. . . . . . . . . . . . . 14 |- ([_z / x]_X e. B -> A.x[_z / x]_X e. B)
46		csbeq1a 2546	. . . . . . . . . . . . . . 15 |- (x = z -> X = [_z / x]_X)
47	46	eleq1d 1963	. . . . . . . . . . . . . 14 |- (x = z -> (X e. B <-> [_z / x]_X e. B))
48	45, 47	rcla4 2373	. . . . . . . . . . . . 13 |- (z e. A -> (A.x e. A X e. B -> [_z / x]_X e. B))
49	48	com12 14	. . . . . . . . . . . 12 |- (A.x e. A X e. B -> (z e. A -> [_z / x]_X e. B))
50	33, 41, 49	3anim123d 1175	. . . . . . . . . . 11 |- (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)))
51	50	imp 377	. . . . . . . . . 10 |- ((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))
52	51	adantll 428	. . . . . . . . 9 |- (((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))
53		potr 3598	. . . . . . . . . . 11 |- ((R Po B /\ ([_v / x]_X e. B /\ [_w / x]_X e. B /\ [_z / x]_X e. B)) -> (([_v / x]_XR[_w / x]_X /\ [_w / x]_XR[_z / x]_X) -> [_v / x]_XR[_z / x]_X))
54		df-br 3339	. . . . . . . . . . . . 13 |- (vSw <-> <.v, w>. e. S)
55	3	eleq2i 1961	. . . . . . . . . . . . 13 |- (<.v, w>. e. S <-> <.v, w>. e. {<.x, y>. | XRY})
56		ax-17 1317	. . . . . . . . . . . . . 14 |- ([_v / x]_XR[_w / x]_X -> A.y[_v / x]_XR[_w / x]_X)
57		csbeq1 2542	. . . . . . . . . . . . . . . 16 |- (y = w -> [_y / x]_X = [_w / x]_X)
58	57, 17	syl5eqr 1942	. . . . . . . . . . . . . . 15 |- (y = w -> Y = [_w / x]_X)
59	58	breq2d 3350	. . . . . . . . . . . . . 14 |- (y = w -> ([_v / x]_XRY <-> [_v / x]_XR[_w / x]_X))
60	10, 56, 5, 34, 13, 59	opelopabf 3572	. . . . . . . . . . . . 13 |- (<.v, w>. e. {<.x, y>. | XRY} <-> [_v / x]_XR[_w / x]_X)
61	54, 55, 60	3bitri 194	. . . . . . . . . . . 12 |- (vSw <-> [_v / x]_XR[_w / x]_X)
62		df-br 3339	. . . . . . . . . . . . 13 |- (wSz <-> <.w, z>. e. S)
63	3	eleq2i 1961	. . . . . . . . . . . . 13 |- (<.w, z>. e. S <-> <.w, z>. e. {<.x, y>. | XRY})
64	36, 8, 9	hbbr 3381	. . . . . . . . . . . . . 14 |- ([_w / x]_XRY -> A.x[_w / x]_XRY)
65		ax-17 1317	. . . . . . . . . . . . . 14 |- ([_w / x]_XR[_z / x]_X -> A.y[_w / x]_XR[_z / x]_X)
66	38	breq1d 3348	. . . . . . . . . . . . . 14 |- (x = w -> (XRY <-> [_w / x]_XRY))
67		csbeq1 2542	. . . . . . . . . . . . . . . 16 |- (y = z -> [_y / x]_X = [_z / x]_X)
68	67, 17	syl5eqr 1942	. . . . . . . . . . . . . . 15 |- (y = z -> Y = [_z / x]_X)
69	68	breq2d 3350	. . . . . . . . . . . . . 14 |- (y = z -> ([_w / x]_XRY <-> [_w / x]_XR[_z / x]_X))
70	64, 65, 34, 42, 66, 69	opelopabf 3572	. . . . . . . . . . . . 13 |- (<.w, z>. e. {<.x, y>. | XRY} <-> [_w / x]_XR[_z / x]_X)
71	62, 63, 70	3bitri 194	. . . . . . . . . . . 12 |- (wSz <-> [_w / x]_XR[_z / x]_X)
72	61, 71	anbi12i 540	. . . . . . . . . . 11 |- ((vSw /\ wSz) <-> ([_v / x]_XR[_w / x]_X /\ [_w / x]_XR[_z / x]_X))
73		df-br 3339	. . . . . . . . . . . 12 |- (vSz <-> <.v, z>. e. S)
74	3	eleq2i 1961	. . . . . . . . . . . 12 |- (<.v, z>. e. S <-> <.v, z>. e. {<.x, y>. | XRY})
75		ax-17 1317	. . . . . . . . . . . . 13 |- ([_v / x]_XR[_z / x]_X -> A.y[_v / x]_XR[_z / x]_X)
76	68	breq2d 3350	. . . . . . . . . . . . 13 |- (y = z -> ([_v / x]_XRY <-> [_v / x]_XR[_z / x]_X))
77	10, 75, 5, 42, 13, 76	opelopabf 3572	. . . . . . . . . . . 12 |- (<.v, z>. e. {<.x, y>. | XRY} <-> [_v / x]_XR[_z / x]_X)
78	73, 74, 77	3bitri 194	. . . . . . . . . . 11 |- (vSz <-> [_v / x]_XR[_z / x]_X)
79	53, 72, 78	3imtr4g 612	. . . . . . . . . 10 |- ((R Po B /\ ([_v / x]_X e. B /\ [_w / x]_X e. B /\ [_z / x]_X e. B)) -> ((vSw /\ wSz) -> vSz))
80	79	adantlr 429	. . . . . . . . 9 |- (((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)) -> ((vSw /\ wSz) -> vSz))
81	52, 80	syldan 516	. . . . . . . 8 |- (((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A /\ z e. A)) -> ((vSw /\ wSz) -> vSz))
82		df-3an 860	. . . . . . . 8 |- ((v e. A /\ w e. A /\ z e. A) <-> ((v e. A /\ w e. A) /\ z e. A))
83	81, 82	sylan2br 502	. . . . . . 7 |- (((R Po B /\ A.x e. A X e. B) /\ ((v e. A /\ w e. A) /\ z e. A)) -> ((vSw /\ wSz) -> vSz))
84	83	anassrs 489	. . . . . 6 |- ((((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A)) /\ z e. A) -> ((vSw /\ wSz) -> vSz))
85	32, 84	jca 310	. . . . 5 |- ((((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A)) /\ z e. A) -> (-. vSv /\ ((vSw /\ wSz) -> vSz)))
86	85	r19.21aiva 2176	. . . 4 |- (((R Po B /\ A.x e. A X e. B) /\ (v e. A /\ w e. A)) -> A.z e. A (-. vSv /\ ((vSw /\ wSz) -> vSz)))
87	86	ex 402	. . 3 |- ((R Po B /\ A.x e. A X e. B) -> ((v e. A /\ w e. A) -> A.z e. A (-. vSv /\ ((vSw /\ wSz) -> vSz))))
88	87	r19.21aivv 2183	. 2 |- ((R Po B /\ A.x e. A X e. B) -> A.v e. A A.w e. A A.z e. A (-. vSv /\ ((vSw /\ wSz) -> vSz)))
89		df-po 3591	. 2 |- (S Po A <-> A.v e. A A.w e. A A.z e. A (-. vSv /\ ((vSw /\ wSz) -> vSz)))
90	88, 89	sylibr 217	1 |- ((R Po B /\ A.x e. A X e. B) -> S Po A)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  [_csb 2540  <.cop 3046   class class class wbr 3338  {copab 3395   Po wpo 3589

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-po 3591

Copyright terms: Public domain