Theorem pospropd 17134

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
pospropd	|- ( ph -> ( K e. Poset <-> L e. Poset ) )

Distinct variable groups:   x, B, y   ph, x, y   x, K, y   x, L, y

Allowed substitution hints:   V( x, y)   W( x, y)

Proof of Theorem pospropd

Dummy variables a b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pospropd.xy	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( le ` K ) y <-> x ( le ` L ) y ) )
2	1	ralrimivva 2971	. . . . . . . . . 10 |- ( ph -> A. x e. B A. y e. B ( x ( le ` K ) y <-> x ( le ` L ) y ) )
3		simp1 1061	. . . . . . . . . . . . 13 |- ( ( a e. B /\ b e. B /\ c e. B ) -> a e. B )
4	3, 3	jca 554	. . . . . . . . . . . 12 |- ( ( a e. B /\ b e. B /\ c e. B ) -> ( a e. B /\ a e. B ) )
5		breq1 4656	. . . . . . . . . . . . . 14 |- ( x = a -> ( x ( le ` K ) y <-> a ( le ` K ) y ) )
6		breq1 4656	. . . . . . . . . . . . . 14 |- ( x = a -> ( x ( le ` L ) y <-> a ( le ` L ) y ) )
7	5, 6	bibi12d 335	. . . . . . . . . . . . 13 |- ( x = a -> ( ( x ( le ` K ) y <-> x ( le ` L ) y ) <-> ( a ( le ` K ) y <-> a ( le ` L ) y ) ) )
8		breq2 4657	. . . . . . . . . . . . . 14 |- ( y = a -> ( a ( le ` K ) y <-> a ( le ` K ) a ) )
9		breq2 4657	. . . . . . . . . . . . . 14 |- ( y = a -> ( a ( le ` L ) y <-> a ( le ` L ) a ) )
10	8, 9	bibi12d 335	. . . . . . . . . . . . 13 |- ( y = a -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) a <-> a ( le ` L ) a ) ) )
11	7, 10	rspc2va 3323	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
12	4, 11	sylan 488	. . . . . . . . . . 11 |- ( ( ( 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 ) )
13		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = b -> ( a ( le ` K ) y <-> a ( le ` K ) b ) )
14		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = b -> ( a ( le ` L ) y <-> a ( le ` L ) b ) )
15	13, 14	bibi12d 335	. . . . . . . . . . . . . . 15 |- ( y = b -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) b <-> a ( le ` L ) b ) ) )
16	7, 15	rspc2va 3323	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
17	16	3adantl3 1219	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
18		3simpb 1059	. . . . . . . . . . . . . . 15 |- ( ( b e. B /\ c e. B /\ a e. B ) -> ( b e. B /\ a e. B ) )
19	18	3comr 1273	. . . . . . . . . . . . . 14 |- ( ( a e. B /\ b e. B /\ c e. B ) -> ( b e. B /\ a e. B ) )
20		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( x = b -> ( x ( le ` K ) y <-> b ( le ` K ) y ) )
21		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( x = b -> ( x ( le ` L ) y <-> b ( le ` L ) y ) )
22	20, 21	bibi12d 335	. . . . . . . . . . . . . . 15 |- ( x = b -> ( ( x ( le ` K ) y <-> x ( le ` L ) y ) <-> ( b ( le ` K ) y <-> b ( le ` L ) y ) ) )
23		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = a -> ( b ( le ` K ) y <-> b ( le ` K ) a ) )
24		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = a -> ( b ( le ` L ) y <-> b ( le ` L ) a ) )
25	23, 24	bibi12d 335	. . . . . . . . . . . . . . 15 |- ( y = a -> ( ( b ( le ` K ) y <-> b ( le ` L ) y ) <-> ( b ( le ` K ) a <-> b ( le ` L ) a ) ) )
26	22, 25	rspc2va 3323	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
27	19, 26	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
28	17, 27	anbi12d 747	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
29	28	imbi1d 331	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
30		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = c -> ( b ( le ` K ) y <-> b ( le ` K ) c ) )
31		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( y = c -> ( b ( le ` L ) y <-> b ( le ` L ) c ) )
32	30, 31	bibi12d 335	. . . . . . . . . . . . . . 15 |- ( y = c -> ( ( b ( le ` K ) y <-> b ( le ` L ) y ) <-> ( b ( le ` K ) c <-> b ( le ` L ) c ) ) )
33	22, 32	rspc2va 3323	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
34	33	3adantl1 1217	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
35	17, 34	anbi12d 747	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
36		3simpb 1059	. . . . . . . . . . . . 13 |- ( ( a e. B /\ b e. B /\ c e. B ) -> ( a e. B /\ c e. B ) )
37		breq2 4657	. . . . . . . . . . . . . . 15 |- ( y = c -> ( a ( le ` K ) y <-> a ( le ` K ) c ) )
38		breq2 4657	. . . . . . . . . . . . . . 15 |- ( y = c -> ( a ( le ` L ) y <-> a ( le ` L ) c ) )
39	37, 38	bibi12d 335	. . . . . . . . . . . . . 14 |- ( y = c -> ( ( a ( le ` K ) y <-> a ( le ` L ) y ) <-> ( a ( le ` K ) c <-> a ( le ` L ) c ) ) )
40	7, 39	rspc2va 3323	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
41	36, 40	sylan 488	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
42	35, 41	imbi12d 334	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
43	12, 29, 42	3anbi123d 1399	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
44	2, 43	sylan2 491	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
45	44	ancoms 469	. . . . . . . 8 |- ( ( 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 ) ) ) )
46	45	3exp2 1285	. . . . . . 7 |- ( 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 ) ) ) ) ) ) )
47	46	imp42 620	. . . . . 6 |- ( ( ( 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 ) ) ) )
48	47	ralbidva 2985	. . . . 5 |- ( ( 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 ) ) ) )
49	48	2ralbidva 2988	. . . 4 |- ( 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 ) ) ) )
50		pospropd.kb	. . . . 5 |- ( ph -> B = ( Base ` K ) )
51		raleq 3138	. . . . . . 7 |- ( 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 ) ) ) )
52	51	raleqbi1dv 3146	. . . . . 6 |- ( 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 ) ) ) )
53	52	raleqbi1dv 3146	. . . . 5 |- ( 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 ) ) ) )
54	50, 53	syl 17	. . . 4 |- ( 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 ) ) ) )
55		pospropd.lb	. . . . 5 |- ( ph -> B = ( Base ` L ) )
56		raleq 3138	. . . . . . 7 |- ( 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 ) ) ) )
57	56	raleqbi1dv 3146	. . . . . 6 |- ( 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 ) ) ) )
58	57	raleqbi1dv 3146	. . . . 5 |- ( 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 ) ) ) )
59	55, 58	syl 17	. . . 4 |- ( 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 ) ) ) )
60	49, 54, 59	3bitr3d 298	. . 3 |- ( 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 ) ) ) )
61		pospropd.kv	. . . . 5 |- ( ph -> K e. V )
62	61	elexd 3214	. . . 4 |- ( ph -> K e. _V )
63	62	biantrurd 529	. . 3 |- ( 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 ) ) ) ) )
64		pospropd.lv	. . . . 5 |- ( ph -> L e. W )
65	64	elexd 3214	. . . 4 |- ( ph -> L e. _V )
66	65	biantrurd 529	. . 3 |- ( 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	60, 63, 66	3bitr3d 298	. 2 |- ( 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 2622	. . 3 |- ( Base ` K ) = ( Base ` K )
69		eqid 2622	. . 3 |- ( le ` K ) = ( le ` K )
70	68, 69	ispos 16947	. 2 |- ( 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 2622	. . 3 |- ( Base ` L ) = ( Base ` L )
72		eqid 2622	. . 3 |- ( le ` L ) = ( le ` L )
73	71, 72	ispos 16947	. 2 |- ( 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 303	1 |- ( ph -> ( K e. Poset <-> L e. Poset ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   class class class wbr 4653   ` cfv 5888   Basecbs 15857   lecple 15948   Posetcpo 16940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-poset 16946

This theorem is referenced by:  oduposb  17136