Theorem pocl 4031

Description: Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)

Assertion

Ref	Expression
pocl	|- ( R Po A -> ((B e. A /\ C e. A /\ D e. A) -> (-. B RB /\ ((B R C /\ C R D) -> B R D))))

Proof of Theorem pocl

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 19	. . . . . . 7 |- (x = B -> x = B)
2	1, 1	breq12d 3768	. . . . . 6 |- (x = B -> (x Rx <-> B RB))
3	2	notbid 591	. . . . 5 |- (x = B -> (-. x Rx <-> -. B RB))
4		breq1 3758	. . . . . . 7 |- (x = B -> (x Ry <-> B Ry))
5	4	anbi1d 438	. . . . . 6 |- (x = B -> ((x Ry /\ y Rz) <-> (B Ry /\ y Rz)))
6		breq1 3758	. . . . . 6 |- (x = B -> (x Rz <-> B Rz))
7	5, 6	imbi12d 223	. . . . 5 |- (x = B -> (((x Ry /\ y Rz) -> x Rz) <-> ((B Ry /\ y Rz) -> B Rz)))
8	3, 7	anbi12d 442	. . . 4 |- (x = B -> ((-. x Rx /\ ((x Ry /\ y Rz) -> x Rz)) <-> (-. B RB /\ ((B Ry /\ y Rz) -> B Rz))))
9	8	imbi2d 219	. . 3 |- (x = B -> (( R Po A -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))) <-> ( R Po A -> (-. B RB /\ ((B Ry /\ y Rz) -> B Rz)))))
10		breq2 3759	. . . . . . 7 |- (y = C -> (B Ry <-> B R C))
11		breq1 3758	. . . . . . 7 |- (y = C -> (y Rz <-> C Rz))
12	10, 11	anbi12d 442	. . . . . 6 |- (y = C -> ((B Ry /\ y Rz) <-> (B R C /\ C Rz)))
13	12	imbi1d 220	. . . . 5 |- (y = C -> (((B Ry /\ y Rz) -> B Rz) <-> ((B R C /\ C Rz) -> B Rz)))
14	13	anbi2d 437	. . . 4 |- (y = C -> ((-. B RB /\ ((B Ry /\ y Rz) -> B Rz)) <-> (-. B RB /\ ((B R C /\ C Rz) -> B Rz))))
15	14	imbi2d 219	. . 3 |- (y = C -> (( R Po A -> (-. B RB /\ ((B Ry /\ y Rz) -> B Rz))) <-> ( R Po A -> (-. B RB /\ ((B R C /\ C Rz) -> B Rz)))))
16		breq2 3759	. . . . . . 7 |- (z = D -> ( C Rz <-> C R D))
17	16	anbi2d 437	. . . . . 6 |- (z = D -> ((B R C /\ C Rz) <-> (B R C /\ C R D)))
18		breq2 3759	. . . . . 6 |- (z = D -> (B Rz <-> B R D))
19	17, 18	imbi12d 223	. . . . 5 |- (z = D -> (((B R C /\ C Rz) -> B Rz) <-> ((B R C /\ C R D) -> B R D)))
20	19	anbi2d 437	. . . 4 |- (z = D -> ((-. B RB /\ ((B R C /\ C Rz) -> B Rz)) <-> (-. B RB /\ ((B R C /\ C R D) -> B R D))))
21	20	imbi2d 219	. . 3 |- (z = D -> (( R Po A -> (-. B RB /\ ((B R C /\ C Rz) -> B Rz))) <-> ( R Po A -> (-. B RB /\ ((B R C /\ C R D) -> B R D)))))
22		df-po 4024	. . . . . . . 8 |- ( R Po A <-> A.x e. A A.y e. A A.z e. A (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz)))
23		r3al 2360	. . . . . . . 8 |- (A.x e. A A.y e. A A.z e. A (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz)) <-> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
24	22, 23	bitri 173	. . . . . . 7 |- ( R Po A <-> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
25	24	biimpi 113	. . . . . 6 |- ( R Po A -> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
26	25	19.21bbi 1448	. . . . 5 |- ( R Po A -> A.z((x e. A /\ y e. A /\ z e. A) -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
27	26	19.21bi 1447	. . . 4 |- ( R Po A -> ((x e. A /\ y e. A /\ z e. A) -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
28	27	com12 27	. . 3 |- ((x e. A /\ y e. A /\ z e. A) -> ( R Po A -> (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz))))
29	9, 15, 21, 28	vtocl3ga 2617	. 2 |- ((B e. A /\ C e. A /\ D e. A) -> ( R Po A -> (-. B RB /\ ((B R C /\ C R D) -> B R D))))
30	29	com12 27	1 |- ( R Po A -> ((B e. A /\ C e. A /\ D e. A) -> (-. B RB /\ ((B R C /\ C R D) -> B R D))))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   /\ w3a 884  A.wal 1240   = wceq 1242   e. wcel 1390  A.wral 2300   class class class wbr 3755   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-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-po 4024

This theorem is referenced by:  poirr  4035  potr  4036