Metamath Proof Explorer


Theorem 4atexlemqtb

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
4thatlempqb.j ˙ = join K
4thatlempqb.a A = Atoms K
Assertion 4atexlemqtb φ Q ˙ T Base K

Proof

Step Hyp Ref Expression
1 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
2 4thatlempqb.j ˙ = join K
3 4thatlempqb.a A = Atoms K
4 1 4atexlemk φ K HL
5 1 4atexlemq φ Q A
6 1 4atexlemt φ T A
7 eqid Base K = Base K
8 7 2 3 hlatjcl K HL Q A T A Q ˙ T Base K
9 4 5 6 8 syl3anc φ Q ˙ T Base K