Metamath Proof Explorer


Theorem 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 ˙ = K
isopos.o ˙ = oc K
isopos.j ˙ = join K
isopos.m ˙ = meet K
isopos.f 0 ˙ = 0. K
isopos.u 1 ˙ = 1. K
Assertion isopos K OP K Poset B dom U B dom G x B y B ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 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 ˙ = K
5 isopos.o ˙ = oc K
6 isopos.j ˙ = join K
7 isopos.m ˙ = meet K
8 isopos.f 0 ˙ = 0. K
9 isopos.u 1 ˙ = 1. K
10 fveq2 p = K Base p = Base K
11 10 1 eqtr4di p = K Base p = B
12 fveq2 p = K lub p = lub K
13 12 2 eqtr4di p = K lub p = U
14 13 dmeqd p = K dom lub p = dom U
15 11 14 eleq12d p = K Base p dom lub p B dom U
16 fveq2 p = K glb p = glb K
17 16 3 eqtr4di p = K glb p = G
18 17 dmeqd p = K dom glb p = dom G
19 11 18 eleq12d p = K Base p dom glb p B dom G
20 15 19 anbi12d p = K Base p dom lub p Base p dom glb p B dom U B dom G
21 fveq2 p = K oc p = oc K
22 21 5 eqtr4di p = K oc p = ˙
23 22 eqeq2d p = K n = oc p n = ˙
24 11 eleq2d p = K n x Base p n x B
25 fveq2 p = K p = K
26 25 4 eqtr4di p = K p = ˙
27 26 breqd p = K x p y x ˙ y
28 26 breqd p = K n y p n x n y ˙ n x
29 27 28 imbi12d p = K x p y n y p n x x ˙ y n y ˙ n x
30 24 29 3anbi13d p = K n x Base p n n x = x x p y n y p n x n x B n n x = x x ˙ y n y ˙ n x
31 fveq2 p = K join p = join K
32 31 6 eqtr4di p = K join p = ˙
33 32 oveqd p = K x join p n x = x ˙ n x
34 fveq2 p = K 1. p = 1. K
35 34 9 eqtr4di p = K 1. p = 1 ˙
36 33 35 eqeq12d p = K x join p n x = 1. p x ˙ n x = 1 ˙
37 fveq2 p = K meet p = meet K
38 37 7 eqtr4di p = K meet p = ˙
39 38 oveqd p = K x meet p n x = x ˙ n x
40 fveq2 p = K 0. p = 0. K
41 40 8 eqtr4di p = K 0. p = 0 ˙
42 39 41 eqeq12d p = K x meet p n x = 0. p x ˙ n x = 0 ˙
43 30 36 42 3anbi123d p = K n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
44 11 43 raleqbidv p = K y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
45 11 44 raleqbidv p = K x Base p y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
46 23 45 anbi12d p = K n = oc p x Base p y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
47 46 exbidv p = K n n = oc p x Base p y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
48 20 47 anbi12d p = K Base p dom lub p Base p dom glb p n n = oc p x Base p y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p B dom U B dom G n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
49 df-oposet OP = p Poset | Base p dom lub p Base p dom glb p n n = oc p x Base p y Base p n x Base p n n x = x x p y n y p n x x join p n x = 1. p x meet p n x = 0. p
50 48 49 elrab2 K OP K Poset B dom U B dom G n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
51 anass K Poset B dom U B dom G n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙ K Poset B dom U B dom G n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙
52 3anass K Poset B dom U B dom G K Poset B dom U B dom G
53 52 bicomi K Poset B dom U B dom G K Poset B dom U B dom G
54 5 fvexi ˙ V
55 fveq1 n = ˙ n x = ˙ x
56 55 eleq1d n = ˙ n x B ˙ x B
57 id n = ˙ n = ˙
58 57 55 fveq12d n = ˙ n n x = ˙ ˙ x
59 58 eqeq1d n = ˙ n n x = x ˙ ˙ x = x
60 fveq1 n = ˙ n y = ˙ y
61 60 55 breq12d n = ˙ n y ˙ n x ˙ y ˙ ˙ x
62 61 imbi2d n = ˙ x ˙ y n y ˙ n x x ˙ y ˙ y ˙ ˙ x
63 56 59 62 3anbi123d n = ˙ n x B n n x = x x ˙ y n y ˙ n x ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x
64 55 oveq2d n = ˙ x ˙ n x = x ˙ ˙ x
65 64 eqeq1d n = ˙ x ˙ n x = 1 ˙ x ˙ ˙ x = 1 ˙
66 55 oveq2d n = ˙ x ˙ n x = x ˙ ˙ x
67 66 eqeq1d n = ˙ x ˙ n x = 0 ˙ x ˙ ˙ x = 0 ˙
68 63 65 67 3anbi123d n = ˙ n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙ ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 0 ˙
69 68 2ralbidv n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙ x B y B ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 0 ˙
70 54 69 ceqsexv n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙ x B y B ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 0 ˙
71 53 70 anbi12i K Poset B dom U B dom G n n = ˙ x B y B n x B n n x = x x ˙ y n y ˙ n x x ˙ n x = 1 ˙ x ˙ n x = 0 ˙ K Poset B dom U B dom G x B y B ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 0 ˙
72 50 51 71 3bitr2i K OP K Poset B dom U B dom G x B y B ˙ x B ˙ ˙ x = x x ˙ y ˙ y ˙ ˙ x x ˙ ˙ x = 1 ˙ x ˙ ˙ x = 0 ˙