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	$⊢ φ \to K \in V$
	pospropd.lv	$⊢ φ \to L \in W$
	pospropd.kb	$⊢ φ \to B = {Base}_{K}$
	pospropd.lb	$⊢ φ \to B = {Base}_{L}$
	pospropd.xy	$⊢ (φ \land (x \in B \land y \in B)) \to (x \leq_{K} y \leftrightarrow x \leq_{L} y)$
Assertion	pospropd	$⊢ φ \to (K \in Poset \leftrightarrow L \in Poset)$

Proof

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

Metamath Proof Explorer

Theorem pospropd

Proof