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

Metamath Proof Explorer

Theorem cdlemkj-2N

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

Ref Expression
Hypotheses cdlemk2.b ⊢ B = Base K
cdlemk2.l ⊢ ≤ ˙ = ≤ K
cdlemk2.j ⊢ ∨ ˙ = join ⁡ K
cdlemk2.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk2.a ⊢ A = Atoms ⁡ K
cdlemk2.h ⊢ H = LHyp ⁡ K
cdlemk2.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk2.r ⊢ R = trL ⁡ K ⁡ W
cdlemk2.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
cdlemk2.q ⊢ Q = S ⁡ C
cdlemk.y ⊢ Y = ι k ∈ T | k ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ G ∘ C -1
Assertion cdlemkj-2N ⊢ K ∈ HL ∧ W ∈ H ∧ R ⁡ F = R ⁡ N ∧ G ∈ T ∧ F ∈ T ∧ C ∈ T ∧ N ∈ T ∧ R ⁡ C ≠ R ⁡ F ∧ R ⁡ C ≠ R ⁡ G ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ C ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → Y ∈ T

Proof

Step Hyp Ref Expression
1 cdlemk2.b ⊢ B = Base K
2 cdlemk2.l ⊢ ≤ ˙ = ≤ K
3 cdlemk2.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk2.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk2.a ⊢ A = Atoms ⁡ K
6 cdlemk2.h ⊢ H = LHyp ⁡ K
7 cdlemk2.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk2.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk2.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
10 cdlemk2.q ⊢ Q = S ⁡ C
11 cdlemk.y ⊢ Y = ι k ∈ T | k ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ G ∘ C -1
12 1 2 3 4 5 6 7 8 9 10 11 cdlemkj ⊢ K ∈ HL ∧ W ∈ H ∧ R ⁡ F = R ⁡ N ∧ G ∈ T ∧ F ∈ T ∧ C ∈ T ∧ N ∈ T ∧ R ⁡ C ≠ R ⁡ F ∧ R ⁡ C ≠ R ⁡ G ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ C ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → Y ∈ T