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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
isopos.e ⊢ 𝑈 = ( lub ‘ 𝐾 )
isopos.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
isopos.l ⊢ ≤ = ( le ‘ 𝐾 )
isopos.o ⊢ ⊥ = ( oc ‘ 𝐾 )
isopos.j ⊢ ∨ = ( join ‘ 𝐾 )
isopos.m ⊢ ∧ = ( meet ‘ 𝐾 )
isopos.f ⊢ 0 = ( 0. ‘ 𝐾 )
isopos.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion isopos ( 𝐾 ∈ OP ↔ ( ( 𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 isopos.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isopos.e ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 isopos.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 isopos.l ⊢ ≤ = ( le ‘ 𝐾 )
5 isopos.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 isopos.j ⊢ ∨ = ( join ‘ 𝐾 )
7 isopos.m ⊢ ∧ = ( meet ‘ 𝐾 )
8 isopos.f ⊢ 0 = ( 0. ‘ 𝐾 )
9 isopos.u ⊢ 1 = ( 1. ‘ 𝐾 )
10 fveq2 ⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
11 10 1 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
12 fveq2 ⊢ ( 𝑝 = 𝐾 → ( lub ‘ 𝑝 ) = ( lub ‘ 𝐾 ) )
13 12 2 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( lub ‘ 𝑝 ) = 𝑈 )
14 13 dmeqd ⊢ ( 𝑝 = 𝐾 → dom ( lub ‘ 𝑝 ) = dom 𝑈 )
15 11 14 eleq12d ⊢ ( 𝑝 = 𝐾 → ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ↔ 𝐵 ∈ dom 𝑈 ) )
16 fveq2 ⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = ( glb ‘ 𝐾 ) )
17 16 3 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = 𝐺 )
18 17 dmeqd ⊢ ( 𝑝 = 𝐾 → dom ( glb ‘ 𝑝 ) = dom 𝐺 )
19 11 18 eleq12d ⊢ ( 𝑝 = 𝐾 → ( ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ↔ 𝐵 ∈ dom 𝐺 ) )
20 15 19 anbi12d ⊢ ( 𝑝 = 𝐾 → ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ↔ ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ) )
21 fveq2 ⊢ ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = ( oc ‘ 𝐾 ) )
22 21 5 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = ⊥ )
23 22 eqeq2d ⊢ ( 𝑝 = 𝐾 → ( 𝑛 = ( oc ‘ 𝑝 ) ↔ 𝑛 = ⊥ ) )
24 11 eleq2d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ↔ ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ) )
25 fveq2 ⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) )
26 25 4 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ≤ )
27 26 breqd ⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( le ‘ 𝑝 ) 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
28 26 breqd ⊢ ( 𝑝 = 𝐾 → ( ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ↔ ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) )
29 27 28 imbi12d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) )
30 24 29 3anbi13d ⊢ ( 𝑝 = 𝐾 → ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ↔ ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ) )
31 fveq2 ⊢ ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = ( join ‘ 𝐾 ) )
32 31 6 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = ∨ )
33 32 oveqd ⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) )
34 fveq2 ⊢ ( 𝑝 = 𝐾 → ( 1. ‘ 𝑝 ) = ( 1. ‘ 𝐾 ) )
35 34 9 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( 1. ‘ 𝑝 ) = 1 )
36 33 35 eqeq12d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ↔ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ) )
37 fveq2 ⊢ ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = ( meet ‘ 𝐾 ) )
38 37 7 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = ∧ )
39 38 oveqd ⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) )
40 fveq2 ⊢ ( 𝑝 = 𝐾 → ( 0. ‘ 𝑝 ) = ( 0. ‘ 𝐾 ) )
41 40 8 eqtr4di ⊢ ( 𝑝 = 𝐾 → ( 0. ‘ 𝑝 ) = 0 )
42 39 41 eqeq12d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ↔ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) )
43 30 36 42 3anbi123d ⊢ ( 𝑝 = 𝐾 → ( ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ↔ ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) )
44 11 43 raleqbidv ⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) )
45 11 44 raleqbidv ⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑝 ) ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) )
46 23 45 anbi12d ⊢ ( 𝑝 = 𝐾 → ( ( 𝑛 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑝 ) ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ) ↔ ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) )
47 46 exbidv ⊢ ( 𝑝 = 𝐾 → ( ∃ 𝑛 ( 𝑛 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑝 ) ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ) ↔ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) )
48 20 47 anbi12d ⊢ ( 𝑝 = 𝐾 → ( ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑛 ( 𝑛 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑝 ) ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ) ) ↔ ( ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) ) )
49 df-oposet ⊢ OP = { 𝑝 ∈ Poset ∣ ( ( ( Base ‘ 𝑝 ) ∈ dom ( lub ‘ 𝑝 ) ∧ ( Base ‘ 𝑝 ) ∈ dom ( glb ‘ 𝑝 ) ) ∧ ∃ 𝑛 ( 𝑛 = ( oc ‘ 𝑝 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑝 ) ∀ 𝑦 ∈ ( Base ‘ 𝑝 ) ( ( ( 𝑛 ‘ 𝑥 ) ∈ ( Base ‘ 𝑝 ) ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ( le ‘ 𝑝 ) 𝑦 → ( 𝑛 ‘ 𝑦 ) ( le ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ( join ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 1. ‘ 𝑝 ) ∧ ( 𝑥 ( meet ‘ 𝑝 ) ( 𝑛 ‘ 𝑥 ) ) = ( 0. ‘ 𝑝 ) ) ) ) }
50 48 49 elrab2 ⊢ ( 𝐾 ∈ OP ↔ ( 𝐾 ∈ Poset ∧ ( ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) ) )
51 anass ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ) ∧ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) ↔ ( 𝐾 ∈ Poset ∧ ( ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) ) )
52 3anass ⊢ ( ( 𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ↔ ( 𝐾 ∈ Poset ∧ ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ) )
53 52 bicomi ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ) ↔ ( 𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) )
54 5 fvexi ⊢ ⊥ ∈ V
55 fveq1 ⊢ ( 𝑛 = ⊥ → ( 𝑛 ‘ 𝑥 ) = ( ⊥ ‘ 𝑥 ) )
56 55 eleq1d ⊢ ( 𝑛 = ⊥ → ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ↔ ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ) )
57 id ⊢ ( 𝑛 = ⊥ → 𝑛 = ⊥ )
58 57 55 fveq12d ⊢ ( 𝑛 = ⊥ → ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) )
59 58 eqeq1d ⊢ ( 𝑛 = ⊥ → ( ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
60 fveq1 ⊢ ( 𝑛 = ⊥ → ( 𝑛 ‘ 𝑦 ) = ( ⊥ ‘ 𝑦 ) )
61 60 55 breq12d ⊢ ( 𝑛 = ⊥ → ( ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ↔ ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) )
62 61 imbi2d ⊢ ( 𝑛 = ⊥ → ( ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) )
63 56 59 62 3anbi123d ⊢ ( 𝑛 = ⊥ → ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ↔ ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ) )
64 55 oveq2d ⊢ ( 𝑛 = ⊥ → ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) )
65 64 eqeq1d ⊢ ( 𝑛 = ⊥ → ( ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ↔ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ) )
66 55 oveq2d ⊢ ( 𝑛 = ⊥ → ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) )
67 66 eqeq1d ⊢ ( 𝑛 = ⊥ → ( ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ↔ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) )
68 63 65 67 3anbi123d ⊢ ( 𝑛 = ⊥ → ( ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ↔ ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) ) )
69 68 2ralbidv ⊢ ( 𝑛 = ⊥ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) ) )
70 54 69 ceqsexv ⊢ ( ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) )
71 53 70 anbi12i ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ) ∧ ∃ 𝑛 ( 𝑛 = ⊥ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝑛 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑛 ‘ ( 𝑛 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( 𝑛 ‘ 𝑦 ) ≤ ( 𝑛 ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( 𝑛 ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( 𝑛 ‘ 𝑥 ) ) = 0 ) ) ) ↔ ( ( 𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) ) )
72 50 51 71 3bitr2i ⊢ ( 𝐾 ∈ OP ↔ ( ( 𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝑥 ≤ 𝑦 → ( ⊥ ‘ 𝑦 ) ≤ ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∨ ( ⊥ ‘ 𝑥 ) ) = 1 ∧ ( 𝑥 ∧ ( ⊥ ‘ 𝑥 ) ) = 0 ) ) )