isopos

Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011) (Revised by NM, 14-Sep-2018)

	Ref	Expression
Hypotheses	isopos.b	$⊢ B = {Base}_{K}$
	isopos.e	$⊢ U = lub (K)$
	isopos.g	$⊢ G = glb (K)$
	isopos.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	isopos.o	$⊢ \underset{˙}{⊥} = oc (K)$
	isopos.j	$⊢ \underset{˙}{\lor} = join (K)$
	isopos.m	$⊢ \underset{˙}{\land} = meet (K)$
	isopos.f	$⊢ \underset{˙}{0} = 0. (K)$
	isopos.u	$⊢ \underset{˙}{1} = 1. (K)$
Assertion	isopos	$⊢ K \in OP \leftrightarrow ((K \in Poset \land B \in dom U \land B \in dom G) \land \forall x \in B \forall y \in B ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		isopos.b	$⊢ B = {Base}_{K}$
2		isopos.e	$⊢ U = lub (K)$
3		isopos.g	$⊢ G = glb (K)$
4		isopos.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
5		isopos.o	$⊢ \underset{˙}{⊥} = oc (K)$
6		isopos.j	$⊢ \underset{˙}{\lor} = join (K)$
7		isopos.m	$⊢ \underset{˙}{\land} = meet (K)$
8		isopos.f	$⊢ \underset{˙}{0} = 0. (K)$
9		isopos.u	$⊢ \underset{˙}{1} = 1. (K)$
10		fveq2	$⊢ p = K \to {Base}_{p} = {Base}_{K}$
11	10 1	syl6eqr	$⊢ p = K \to {Base}_{p} = B$
12		fveq2	$⊢ p = K \to lub (p) = lub (K)$
13	12 2	syl6eqr	$⊢ p = K \to lub (p) = U$
14	13	dmeqd	$⊢ p = K \to dom lub (p) = dom U$
15	11 14	eleq12d	$⊢ p = K \to ({Base}_{p} \in dom lub (p) \leftrightarrow B \in dom U)$
16		fveq2	$⊢ p = K \to glb (p) = glb (K)$
17	16 3	syl6eqr	$⊢ p = K \to glb (p) = G$
18	17	dmeqd	$⊢ p = K \to dom glb (p) = dom G$
19	11 18	eleq12d	$⊢ p = K \to ({Base}_{p} \in dom glb (p) \leftrightarrow B \in dom G)$
20	15 19	anbi12d	$⊢ p = K \to (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \leftrightarrow (B \in dom U \land B \in dom G))$
21		fveq2	$⊢ p = K \to oc (p) = oc (K)$
22	21 5	syl6eqr	$⊢ p = K \to oc (p) = \underset{˙}{⊥}$
23	22	eqeq2d	$⊢ p = K \to (n = oc (p) \leftrightarrow n = \underset{˙}{⊥})$
24	11	eleq2d	$⊢ p = K \to (n (x) \in {Base}_{p} \leftrightarrow n (x) \in B)$
25		fveq2	$⊢ p = K \to \leq_{p} = \leq_{K}$
26	25 4	syl6eqr	$⊢ p = K \to \leq_{p} = \underset{˙}{\leq}$
27	26	breqd	$⊢ p = K \to (x \leq_{p} y \leftrightarrow x \underset{˙}{\leq} y)$
28	26	breqd	$⊢ p = K \to (n (y) \leq_{p} n (x) \leftrightarrow n (y) \underset{˙}{\leq} n (x))$
29	27 28	imbi12d	$⊢ p = K \to ((x \leq_{p} y \to n (y) \leq_{p} n (x)) \leftrightarrow (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x)))$
30	24 29	3anbi13d	$⊢ p = K \to ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \leftrightarrow (n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))))$
31		fveq2	$⊢ p = K \to join (p) = join (K)$
32	31 6	syl6eqr	$⊢ p = K \to join (p) = \underset{˙}{\lor}$
33	32	oveqd	$⊢ p = K \to x join (p) n (x) = x \underset{˙}{\lor} n (x)$
34		fveq2	$⊢ p = K \to 1. (p) = 1. (K)$
35	34 9	syl6eqr	$⊢ p = K \to 1. (p) = \underset{˙}{1}$
36	33 35	eqeq12d	$⊢ p = K \to (x join (p) n (x) = 1. (p) \leftrightarrow x \underset{˙}{\lor} n (x) = \underset{˙}{1})$
37		fveq2	$⊢ p = K \to meet (p) = meet (K)$
38	37 7	syl6eqr	$⊢ p = K \to meet (p) = \underset{˙}{\land}$
39	38	oveqd	$⊢ p = K \to x meet (p) n (x) = x \underset{˙}{\land} n (x)$
40		fveq2	$⊢ p = K \to 0. (p) = 0. (K)$
41	40 8	syl6eqr	$⊢ p = K \to 0. (p) = \underset{˙}{0}$
42	39 41	eqeq12d	$⊢ p = K \to (x meet (p) n (x) = 0. (p) \leftrightarrow x \underset{˙}{\land} n (x) = \underset{˙}{0})$
43	30 36 42	3anbi123d	$⊢ p = K \to (((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p)) \leftrightarrow ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))$
44	11 43	raleqbidv	$⊢ p = K \to (\forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p)) \leftrightarrow \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))$
45	11 44	raleqbidv	$⊢ p = K \to (\forall x \in {Base}_{p} \forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p)) \leftrightarrow \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))$
46	23 45	anbi12d	$⊢ p = K \to ((n = oc (p) \land \forall x \in {Base}_{p} \forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p))) \leftrightarrow (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0})))$
47	46	exbidv	$⊢ p = K \to (\exists n (n = oc (p) \land \forall x \in {Base}_{p} \forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p))) \leftrightarrow \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0})))$
48	20 47	anbi12d	$⊢ p = K \to ((({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists n (n = oc (p) \land \forall x \in {Base}_{p} \forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p)))) \leftrightarrow ((B \in dom U \land B \in dom G) \land \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))))$
49		df-oposet	$⊢ OP = \{p \in Poset \| (({Base}_{p} \in dom lub (p) \land {Base}_{p} \in dom glb (p)) \land \exists n (n = oc (p) \land \forall x \in {Base}_{p} \forall y \in {Base}_{p} ((n (x) \in {Base}_{p} \land n (n (x)) = x \land (x \leq_{p} y \to n (y) \leq_{p} n (x))) \land x join (p) n (x) = 1. (p) \land x meet (p) n (x) = 0. (p))))\}$
50	48 49	elrab2	$⊢ K \in OP \leftrightarrow (K \in Poset \land ((B \in dom U \land B \in dom G) \land \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))))$
51		anass	$⊢ ((K \in Poset \land (B \in dom U \land B \in dom G)) \land \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))) \leftrightarrow (K \in Poset \land ((B \in dom U \land B \in dom G) \land \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))))$
52		3anass	$⊢ (K \in Poset \land B \in dom U \land B \in dom G) \leftrightarrow (K \in Poset \land (B \in dom U \land B \in dom G))$
53	52	bicomi	$⊢ (K \in Poset \land (B \in dom U \land B \in dom G)) \leftrightarrow (K \in Poset \land B \in dom U \land B \in dom G)$
54	5	fvexi	$⊢ \underset{˙}{⊥} \in V$
55		fveq1	$⊢ n = \underset{˙}{⊥} \to n (x) = \underset{˙}{⊥} (x)$
56	55	eleq1d	$⊢ n = \underset{˙}{⊥} \to (n (x) \in B \leftrightarrow \underset{˙}{⊥} (x) \in B)$
57		id	$⊢ n = \underset{˙}{⊥} \to n = \underset{˙}{⊥}$
58	57 55	fveq12d	$⊢ n = \underset{˙}{⊥} \to n (n (x)) = \underset{˙}{⊥} (\underset{˙}{⊥} (x))$
59	58	eqeq1d	$⊢ n = \underset{˙}{⊥} \to (n (n (x)) = x \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
60		fveq1	$⊢ n = \underset{˙}{⊥} \to n (y) = \underset{˙}{⊥} (y)$
61	60 55	breq12d	$⊢ n = \underset{˙}{⊥} \to (n (y) \underset{˙}{\leq} n (x) \leftrightarrow \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))$
62	61	imbi2d	$⊢ n = \underset{˙}{⊥} \to ((x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x)) \leftrightarrow (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x)))$
63	56 59 62	3anbi123d	$⊢ n = \underset{˙}{⊥} \to ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \leftrightarrow (\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))))$
64	55	oveq2d	$⊢ n = \underset{˙}{⊥} \to x \underset{˙}{\lor} n (x) = x \underset{˙}{\lor} \underset{˙}{⊥} (x)$
65	64	eqeq1d	$⊢ n = \underset{˙}{⊥} \to (x \underset{˙}{\lor} n (x) = \underset{˙}{1} \leftrightarrow x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1})$
66	55	oveq2d	$⊢ n = \underset{˙}{⊥} \to x \underset{˙}{\land} n (x) = x \underset{˙}{\land} \underset{˙}{⊥} (x)$
67	66	eqeq1d	$⊢ n = \underset{˙}{⊥} \to (x \underset{˙}{\land} n (x) = \underset{˙}{0} \leftrightarrow x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0})$
68	63 65 67	3anbi123d	$⊢ n = \underset{˙}{⊥} \to (((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}) \leftrightarrow ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0}))$
69	68	2ralbidv	$⊢ n = \underset{˙}{⊥} \to (\forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}) \leftrightarrow \forall x \in B \forall y \in B ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0}))$
70	54 69	ceqsexv	$⊢ \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0})) \leftrightarrow \forall x \in B \forall y \in B ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0})$
71	53 70	anbi12i	$⊢ ((K \in Poset \land (B \in dom U \land B \in dom G)) \land \exists n (n = \underset{˙}{⊥} \land \forall x \in B \forall y \in B ((n (x) \in B \land n (n (x)) = x \land (x \underset{˙}{\leq} y \to n (y) \underset{˙}{\leq} n (x))) \land x \underset{˙}{\lor} n (x) = \underset{˙}{1} \land x \underset{˙}{\land} n (x) = \underset{˙}{0}))) \leftrightarrow ((K \in Poset \land B \in dom U \land B \in dom G) \land \forall x \in B \forall y \in B ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0}))$
72	50 51 71	3bitr2i	$⊢ K \in OP \leftrightarrow ((K \in Poset \land B \in dom U \land B \in dom G) \land \forall x \in B \forall y \in B ((\underset{˙}{⊥} (x) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \land (x \underset{˙}{\leq} y \to \underset{˙}{⊥} (y) \underset{˙}{\leq} \underset{˙}{⊥} (x))) \land x \underset{˙}{\lor} \underset{˙}{⊥} (x) = \underset{˙}{1} \land x \underset{˙}{\land} \underset{˙}{⊥} (x) = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem isopos

Proof