Metamath Proof Explorer

Theorem chirredlem3

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chirred.1 ⊢ 𝐴 ∈ Cℋ
chirred.2 ⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
Assertion chirredlem3 ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ 𝐴 → 𝑟 = 𝑝 ) )

Proof

Step Hyp Ref Expression
1 chirred.1 ⊢ 𝐴 ∈ Cℋ
2 chirred.2 ⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
3 atelch ⊢ ( 𝑞 ∈ HAtoms → 𝑞 ∈ Cℋ )
4 1 chirredlem2 ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = 𝑞 )
5 4 oveq2d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) ) = ( 𝑟 ∨ℋ 𝑞 ) )
6 atelch ⊢ ( 𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
7 6 adantr ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → 𝑟 ∈ Cℋ )
8 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
9 chjcl ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑝 ∨ℋ 𝑞 ) ∈ Cℋ )
10 8 9 sylan ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → ( 𝑝 ∨ℋ 𝑞 ) ∈ Cℋ )
11 10 ad2ant2r ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑝 ∨ℋ 𝑞 ) ∈ Cℋ )
12 id ⊢ ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) )
13 pjoml2 ⊢ ( ( 𝑟 ∈ Cℋ ∧ ( 𝑝 ∨ℋ 𝑞 ) ∈ Cℋ ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) ) = ( 𝑝 ∨ℋ 𝑞 ) )
14 7 11 12 13 syl3an ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) ) = ( 𝑝 ∨ℋ 𝑞 ) )
15 14 3com12 ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) ) = ( 𝑝 ∨ℋ 𝑞 ) )
16 15 3expb ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) ) = ( 𝑝 ∨ℋ 𝑞 ) )
17 5 16 eqtr3d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ∨ℋ 𝑞 ) = ( 𝑝 ∨ℋ 𝑞 ) )
18 17 ineq2d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) )
19 breq2 ⊢ ( 𝑥 = 𝑟 → ( 𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑟 ) )
20 19 2 vtoclga ⊢ ( 𝑟 ∈ Cℋ → 𝐴 𝐶ℋ 𝑟 )
21 breq2 ⊢ ( 𝑥 = 𝑞 → ( 𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑞 ) )
22 21 2 vtoclga ⊢ ( 𝑞 ∈ Cℋ → 𝐴 𝐶ℋ 𝑞 )
23 20 22 anim12i ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞 ) )
24 fh1 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞 ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
25 1 24 mp3anl1 ⊢ ( ( ( 𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞 ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
26 23 25 mpdan ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
27 6 26 sylan ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
28 27 ancoms ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ HAtoms ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
29 28 adantrr ⊢ ( ( 𝑞 ∈ Cℋ ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
30 29 ad2ant2r ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
31 30 adantll ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ ( 𝑟 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
32 breq2 ⊢ ( 𝑥 = 𝑝 → ( 𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑝 ) )
33 32 2 vtoclga ⊢ ( 𝑝 ∈ Cℋ → 𝐴 𝐶ℋ 𝑝 )
34 33 22 anim12i ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞 ) )
35 fh1 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞 ) ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
36 1 35 mp3anl1 ⊢ ( ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞 ) ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
37 34 36 mpdan ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
38 8 37 sylan ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
39 38 ad2ant2r ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
40 39 adantr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
41 18 31 40 3eqtr3d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) = ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) )
42 sseqin2 ⊢ ( 𝑟 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑟 ) = 𝑟 )
43 42 biimpi ⊢ ( 𝑟 ⊆ 𝐴 → ( 𝐴 ∩ 𝑟 ) = 𝑟 )
44 43 ad2antlr ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝐴 ∩ 𝑟 ) = 𝑟 )
45 44 adantl ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ 𝑟 ) = 𝑟 )
46 incom ⊢ ( 𝐴 ∩ 𝑞 ) = ( 𝑞 ∩ 𝐴 )
47 chsh ⊢ ( 𝑞 ∈ Cℋ → 𝑞 ∈ Sℋ )
48 1 chshii ⊢ 𝐴 ∈ Sℋ
49 orthin ⊢ ( ( 𝑞 ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( 𝑞 ∩ 𝐴 ) = 0ℋ ) )
50 47 48 49 sylancl ⊢ ( 𝑞 ∈ Cℋ → ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( 𝑞 ∩ 𝐴 ) = 0ℋ ) )
51 50 imp ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝑞 ∩ 𝐴 ) = 0ℋ )
52 46 51 syl5eq ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝐴 ∩ 𝑞 ) = 0ℋ )
53 52 ad2antlr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ 𝑞 ) = 0ℋ )
54 45 53 oveq12d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( 𝐴 ∩ 𝑟 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) = ( 𝑟 ∨ℋ 0ℋ ) )
55 sseqin2 ⊢ ( 𝑝 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑝 ) = 𝑝 )
56 55 biimpi ⊢ ( 𝑝 ⊆ 𝐴 → ( 𝐴 ∩ 𝑝 ) = 𝑝 )
57 56 adantl ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) → ( 𝐴 ∩ 𝑝 ) = 𝑝 )
58 57 ad2antrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝐴 ∩ 𝑝 ) = 𝑝 )
59 58 53 oveq12d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( 𝐴 ∩ 𝑝 ) ∨ℋ ( 𝐴 ∩ 𝑞 ) ) = ( 𝑝 ∨ℋ 0ℋ ) )
60 41 54 59 3eqtr3d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ∨ℋ 0ℋ ) = ( 𝑝 ∨ℋ 0ℋ ) )
61 chj0 ⊢ ( 𝑟 ∈ Cℋ → ( 𝑟 ∨ℋ 0ℋ ) = 𝑟 )
62 6 61 syl ⊢ ( 𝑟 ∈ HAtoms → ( 𝑟 ∨ℋ 0ℋ ) = 𝑟 )
63 62 ad2antrr ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ∨ℋ 0ℋ ) = 𝑟 )
64 63 adantl ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ∨ℋ 0ℋ ) = 𝑟 )
65 chj0 ⊢ ( 𝑝 ∈ Cℋ → ( 𝑝 ∨ℋ 0ℋ ) = 𝑝 )
66 8 65 syl ⊢ ( 𝑝 ∈ HAtoms → ( 𝑝 ∨ℋ 0ℋ ) = 𝑝 )
67 66 ad3antrrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∨ℋ 0ℋ ) = 𝑝 )
68 60 64 67 3eqtr3d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑟 = 𝑝 )
69 68 exp44 ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ 𝐴 → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → 𝑟 = 𝑝 ) ) ) )
70 69 com34 ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑟 ⊆ 𝐴 → 𝑟 = 𝑝 ) ) ) )
71 3 70 sylanr1 ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑟 ⊆ 𝐴 → 𝑟 = 𝑝 ) ) ) )
72 71 imp32 ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ 𝐴 → 𝑟 = 𝑝 ) )