Metamath Proof Explorer

Theorem chirredlem1

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

Ref Expression
Hypothesis chirred.1 ⊢ 𝐴 ∈ Cℋ
Assertion chirredlem1 ( ( ( 𝑝 ∈ HAtoms ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ )

Proof

Step Hyp Ref Expression
1 chirred.1 ⊢ 𝐴 ∈ Cℋ
2 atelch ⊢ ( 𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
3 chsscon3 ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑟 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) ) )
4 1 3 mpan2 ⊢ ( 𝑟 ∈ Cℋ → ( 𝑟 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) ) )
5 4 biimpa ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝑟 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) )
6 2 5 sylan ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) )
7 sstr2 ⊢ ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) → 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) )
8 6 7 syl5 ⊢ ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) )
9 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
10 atne0 ⊢ ( 𝑟 ∈ HAtoms → 𝑟 ≠ 0ℋ )
11 10 neneqd ⊢ ( 𝑟 ∈ HAtoms → ¬ 𝑟 = 0ℋ )
12 11 ad3antrrr ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ¬ 𝑟 = 0ℋ )
13 simplr ⊢ ( ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) )
14 choccl ⊢ ( 𝑟 ∈ Cℋ → ( ⊥ ‘ 𝑟 ) ∈ Cℋ )
15 2 14 syl ⊢ ( 𝑟 ∈ HAtoms → ( ⊥ ‘ 𝑟 ) ∈ Cℋ )
16 chlej1 ⊢ ( ( ( 𝑝 ∈ Cℋ ∧ ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) )
17 16 3exp1 ⊢ ( 𝑝 ∈ Cℋ → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ → ( 𝑞 ∈ Cℋ → ( 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) ) ) ) )
18 15 17 syl5com ⊢ ( 𝑟 ∈ HAtoms → ( 𝑝 ∈ Cℋ → ( 𝑞 ∈ Cℋ → ( 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) ) ) ) )
19 18 imp42 ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) )
20 19 adantllr ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) )
21 20 adantlr ⊢ ( ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( 𝑝 ∨ℋ 𝑞 ) ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) )
22 13 21 sstrd ⊢ ( ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → 𝑟 ⊆ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) )
23 chlejb2 ⊢ ( ( 𝑞 ∈ Cℋ ∧ ( ⊥ ‘ 𝑟 ) ∈ Cℋ ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) ) )
24 23 ancoms ⊢ ( ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) ) )
25 24 biimpa ⊢ ( ( ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) )
26 15 25 sylanl1 ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) )
27 26 an32s ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ 𝑞 ∈ Cℋ ) → ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) )
28 27 adantrl ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) → ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) )
29 28 ad2antrr ⊢ ( ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → ( ( ⊥ ‘ 𝑟 ) ∨ℋ 𝑞 ) = ( ⊥ ‘ 𝑟 ) )
30 22 29 sseqtrd ⊢ ( ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ∧ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) → 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) )
31 30 ex ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) → 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) ) )
32 chssoc ⊢ ( 𝑟 ∈ Cℋ → ( 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) ↔ 𝑟 = 0ℋ ) )
33 32 biimpd ⊢ ( 𝑟 ∈ Cℋ → ( 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) → 𝑟 = 0ℋ ) )
34 2 33 syl ⊢ ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) → 𝑟 = 0ℋ ) )
35 34 ad3antrrr ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝑟 ) → 𝑟 = 0ℋ ) )
36 31 35 syld ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) → 𝑟 = 0ℋ ) )
37 12 36 mtod ⊢ ( ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) )
38 37 ex ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) )
39 9 38 sylanr1 ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ) )
40 atnssm0 ⊢ ( ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) → ( ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) = 0ℋ ) )
41 incom ⊢ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) = ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) )
42 41 eqeq1i ⊢ ( ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) = 0ℋ ↔ ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ )
43 40 42 bitrdi ⊢ ( ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) → ( ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) )
44 15 43 sylan ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) )
45 44 ad2ant2r ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ) → ( ¬ 𝑝 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) )
46 39 45 sylibd ⊢ ( ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) )
47 46 exp43 ⊢ ( 𝑟 ∈ HAtoms → ( 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) → ( 𝑝 ∈ HAtoms → ( 𝑞 ∈ Cℋ → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) ) ) ) )
48 47 adantr ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) → ( 𝑝 ∈ HAtoms → ( 𝑞 ∈ Cℋ → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) ) ) ) )
49 8 48 sylcom ⊢ ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( 𝑝 ∈ HAtoms → ( 𝑞 ∈ Cℋ → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) ) ) ) )
50 49 com4t ⊢ ( 𝑝 ∈ HAtoms → ( 𝑞 ∈ Cℋ → ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) ) ) ) )
51 50 impd ⊢ ( 𝑝 ∈ HAtoms → ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ ) ) ) )
52 51 imp43 ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ )