This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemkuvN

Description: Part of proof of Lemma K of Crawley p. 118. Value of the sigma_1 (p) function U . (Contributed by NM, 2-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk1.b ⊢ B = Base K
cdlemk1.l ⊢ ≤ ˙ = ≤ K
cdlemk1.j ⊢ ∨ ˙ = join ⁡ K
cdlemk1.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk1.a ⊢ A = Atoms ⁡ K
cdlemk1.h ⊢ H = LHyp ⁡ K
cdlemk1.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk1.r ⊢ R = trL ⁡ K ⁡ W
cdlemk1.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
cdlemk1.o ⊢ O = S ⁡ D
cdlemk1.u ⊢ U = e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ O ⁡ P ∨ ˙ R ⁡ e ∘ D -1
Assertion cdlemkuvN ⊢ G ∈ T → U ⁡ G = ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ O ⁡ P ∨ ˙ R ⁡ G ∘ D -1

Proof

Step Hyp Ref Expression
1 cdlemk1.b ⊢ B = Base K
2 cdlemk1.l ⊢ ≤ ˙ = ≤ K
3 cdlemk1.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk1.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk1.a ⊢ A = Atoms ⁡ K
6 cdlemk1.h ⊢ H = LHyp ⁡ K
7 cdlemk1.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk1.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk1.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
10 cdlemk1.o ⊢ O = S ⁡ D
11 cdlemk1.u ⊢ U = e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ O ⁡ P ∨ ˙ R ⁡ e ∘ D -1
12 1 2 3 5 6 7 8 4 11 cdlemksv ⊢ G ∈ T → U ⁡ G = ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ O ⁡ P ∨ ˙ R ⁡ G ∘ D -1