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

Metamath Proof Explorer

Theorem cdlemk5auN

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 3-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
Assertion cdlemk5auN ⊢ K ∈ HL ∧ W ∈ H ∧ D ∈ T ∧ G ∈ T ∧ X ∈ T ∧ R ⁡ G ≠ R ⁡ D ∧ D ≠ I ↾ B ∧ G ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → D ⁡ P ∨ ˙ R ⁡ D ∧ ˙ D ⁡ P ∨ ˙ R ⁡ G ∘ D -1 ≤ ˙ X ⁡ P ∨ ˙ R ⁡ X ∘ 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 1 2 3 5 6 7 8 4 cdlemk5a ⊢ K ∈ HL ∧ W ∈ H ∧ D ∈ T ∧ G ∈ T ∧ X ∈ T ∧ R ⁡ G ≠ R ⁡ D ∧ D ≠ I ↾ B ∧ G ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → D ⁡ P ∨ ˙ R ⁡ D ∧ ˙ D ⁡ P ∨ ˙ R ⁡ G ∘ D -1 ≤ ˙ X ⁡ P ∨ ˙ R ⁡ X ∘ D -1