Theorem isopos 38652

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

Hypotheses

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

Ref	Expression
isopos	⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥, ⊥ ,𝑦   𝑥,𝐾,𝑦

Allowed substitution hints:   𝑈(𝑥,𝑦)   1 (𝑥,𝑦)   𝐺(𝑥,𝑦)   ∨ (𝑥,𝑦)   ≤ (𝑥,𝑦)   ∧ (𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem isopos

Dummy variables 𝑛 𝑝 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ∀wral 3058   class class class wbr 5148  dom cdm 5678  ‘cfv 6548  (class class class)co 7420  Basecbs 17180  lecple 17240  occoc 17241  Posetcpo 18299  lubclub 18301  glbcglb 18302  joincjn 18303  meetcmee 18304  0.cp0 18415  1.cp1 18416  OPcops 38644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-dm 5688  df-iota 6500  df-fv 6556  df-ov 7423  df-oposet 38648

This theorem is referenced by:  opposet  38653  oposlem  38654  op01dm  38655

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »