Theorem pospropd

Description: Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	pospropd.kv	|- ( ph -> K e. V )
	pospropd.lv	|- ( ph -> L e. W )
	pospropd.kb	|- ( ph -> B = ( Base ` K ) )
	pospropd.lb	|- ( ph -> B = ( Base ` L ) )
	pospropd.xy	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( le ` K ) y <-> x ( le ` L ) y ) )
Assertion	pospropd	|- ( ph -> ( K e. Poset <-> L e. Poset ) )

Proof

Step	Hyp	Ref	Expression
1		pospropd.kv	|- ( ph -> K e. V )
2		pospropd.lv	|- ( ph -> L e. W )
3		pospropd.kb	|- ( ph -> B = ( Base ` K ) )
4		pospropd.lb	|- ( ph -> B = ( Base ` L ) )
5		pospropd.xy	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( le ` K ) y <-> x ( le ` L ) y ) )
6	5	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) )
7		simp1	|- ( ( a e. B /\ b e. B /\ c e. B ) -> a e. B )
8	7 7	jca	|- ( ( a e. B /\ b e. B /\ c e. B ) -> ( a e. B /\ a e. B ) )
9		breq1	|- ( x = a -> ( x ( le ` K ) y <-> a ( le ` K ) y ) )
10		breq1	|- ( x = a -> ( x ( le ` L ) y <-> a ( le ` L ) y ) )
11	9 10	bibi12d	|- ( x = a -> ( ( x ( le ` K ) y <-> x ( le ` L ) y ) <-> ( a ( le ` K ) y <-> a ( le ` L ) y ) ) )
12		breq2	|- ( y = a -> ( a ( le ` K ) y <-> a ( le ` K ) a ) )
13		breq2	|- ( y = a -> ( a ( le ` L ) y <-> a ( le ` L ) a ) )
14	12 13	bibi12d	|- ( y = a -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) a <-> a ( le ` L ) a ) ) )
15	11 14	rspc2va	|- ( ( ( a e. B /\ a e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) a <-> a ( le ` L ) a ) )
16	8 15	sylan	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) a <-> a ( le ` L ) a ) )
17		breq2	|- ( y = b -> ( a ( le ` K ) y <-> a ( le ` K ) b ) )
18		breq2	|- ( y = b -> ( a ( le ` L ) y <-> a ( le ` L ) b ) )
19	17 18	bibi12d	|- ( y = b -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) b <-> a ( le ` L ) b ) ) )
20	11 19	rspc2va	|- ( ( ( a e. B /\ b e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) b <-> a ( le ` L ) b ) )
21	20	3adantl3	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) b <-> a ( le ` L ) b ) )
22		3simpb	|- ( ( b e. B /\ c e. B /\ a e. B ) -> ( b e. B /\ a e. B ) )
23	22	3comr	|- ( ( a e. B /\ b e. B /\ c e. B ) -> ( b e. B /\ a e. B ) )
24		breq1	|- ( x = b -> ( x ( le ` K ) y <-> b ( le ` K ) y ) )
25		breq1	|- ( x = b -> ( x ( le ` L ) y <-> b ( le ` L ) y ) )
26	24 25	bibi12d	|- ( x = b -> ( ( x ( le ` K ) y <-> x ( le ` L ) y ) <-> ( b ( le ` K ) y <-> b ( le ` L ) y ) ) )
27		breq2	|- ( y = a -> ( b ( le ` K ) y <-> b ( le ` K ) a ) )
28		breq2	|- ( y = a -> ( b ( le ` L ) y <-> b ( le ` L ) a ) )
29	27 28	bibi12d	|- ( y = a -> ( ( b ( le ` K ) y <-> b ( le ` L ) y ) <-> ( b ( le ` K ) a <-> b ( le ` L ) a ) ) )
30	26 29	rspc2va	|- ( ( ( b e. B /\ a e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( b ( le ` K ) a <-> b ( le ` L ) a ) )
31	23 30	sylan	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( b ( le ` K ) a <-> b ( le ` L ) a ) )
32	21 31	anbi12d	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( ( a ( le ` K ) b /\ b ( le ` K ) a ) <-> ( a ( le ` L ) b /\ b ( le ` L ) a ) ) )
33	32	imbi1d	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) <-> ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) ) )
34		breq2	|- ( y = c -> ( b ( le ` K ) y <-> b ( le ` K ) c ) )
35		breq2	|- ( y = c -> ( b ( le ` L ) y <-> b ( le ` L ) c ) )
36	34 35	bibi12d	|- ( y = c -> ( ( b ( le ` K ) y <-> b ( le ` L ) y ) <-> ( b ( le ` K ) c <-> b ( le ` L ) c ) ) )
37	26 36	rspc2va	|- ( ( ( b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( b ( le ` K ) c <-> b ( le ` L ) c ) )
38	37	3adantl1	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( b ( le ` K ) c <-> b ( le ` L ) c ) )
39	21 38	anbi12d	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( ( a ( le ` K ) b /\ b ( le ` K ) c ) <-> ( a ( le ` L ) b /\ b ( le ` L ) c ) ) )
40		3simpb	|- ( ( a e. B /\ b e. B /\ c e. B ) -> ( a e. B /\ c e. B ) )
41		breq2	|- ( y = c -> ( a ( le ` K ) y <-> a ( le ` K ) c ) )
42		breq2	|- ( y = c -> ( a ( le ` L ) y <-> a ( le ` L ) c ) )
43	41 42	bibi12d	|- ( y = c -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) c <-> a ( le ` L ) c ) ) )
44	11 43	rspc2va	|- ( ( ( a e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) c <-> a ( le ` L ) c ) )
45	40 44	sylan	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( a ( le ` K ) c <-> a ( le ` L ) c ) )
46	39 45	imbi12d	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) <-> ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) )
47	16 33 46	3anbi123d	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) ) -> ( ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
48	6 47	sylan2	|- ( ( ( a e. B /\ b e. B /\ c e. B ) /\ ph ) -> ( ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
49	48	ancoms	|- ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
50	49	3exp2	|- ( ph -> ( a e. B -> ( b e. B -> ( c e. B -> ( ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) ) ) ) )
51	50	imp42	|- ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ c e. B ) -> ( ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
52	51	ralbidva	|- ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
53	52	2ralbidva	|- ( ph -> ( A. a e. B A. b e. B A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. a e. B A. b e. B A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
54		raleq	|- ( B = ( Base ` K ) -> ( A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) )
55	54	raleqbi1dv	|- ( B = ( Base ` K ) -> ( A. b e. B A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) )
56	55	raleqbi1dv	|- ( B = ( Base ` K ) -> ( A. a e. B A. b e. B A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) )
57	3 56	syl	|- ( ph -> ( A. a e. B A. b e. B A. c e. B ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) )
58		raleq	|- ( B = ( Base ` L ) -> ( A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) <-> A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
59	58	raleqbi1dv	|- ( B = ( Base ` L ) -> ( A. b e. B A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) <-> A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
60	59	raleqbi1dv	|- ( B = ( Base ` L ) -> ( A. a e. B A. b e. B A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) <-> A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
61	4 60	syl	|- ( ph -> ( A. a e. B A. b e. B A. c e. B ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) <-> A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
62	53 57 61	3bitr3d	|- ( ph -> ( A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
63	1	elexd	|- ( ph -> K e. _V )
64	63	biantrurd	|- ( ph -> ( A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) <-> ( K e. _V /\ A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) ) )
65	2	elexd	|- ( ph -> L e. _V )
66	65	biantrurd	|- ( ph -> ( A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) <-> ( L e. _V /\ A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) ) )
67	62 64 66	3bitr3d	|- ( ph -> ( ( K e. _V /\ A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) <-> ( L e. _V /\ A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) ) )
68		eqid	|- ( Base ` K ) = ( Base ` K )
69		eqid	|- ( le ` K ) = ( le ` K )
70	68 69	ispos	|- ( K e. Poset <-> ( K e. _V /\ A. a e. ( Base ` K ) A. b e. ( Base ` K ) A. c e. ( Base ` K ) ( a ( le ` K ) a /\ ( ( a ( le ` K ) b /\ b ( le ` K ) a ) -> a = b ) /\ ( ( a ( le ` K ) b /\ b ( le ` K ) c ) -> a ( le ` K ) c ) ) ) )
71		eqid	|- ( Base ` L ) = ( Base ` L )
72		eqid	|- ( le ` L ) = ( le ` L )
73	71 72	ispos	|- ( L e. Poset <-> ( L e. _V /\ A. a e. ( Base ` L ) A. b e. ( Base ` L ) A. c e. ( Base ` L ) ( a ( le ` L ) a /\ ( ( a ( le ` L ) b /\ b ( le ` L ) a ) -> a = b ) /\ ( ( a ( le ` L ) b /\ b ( le ` L ) c ) -> a ( le ` L ) c ) ) ) )
74	67 70 73	3bitr4g	|- ( ph -> ( K e. Poset <-> L e. Poset ) )