Metamath Proof Explorer

Theorem mdsymlem5

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢ 𝐴 ∈ Cℋ
mdsymlem1.2 ⊢ 𝐵 ∈ Cℋ
mdsymlem1.3 ⊢ 𝐶 = ( 𝐴 ∨ℋ 𝑝 )
Assertion mdsymlem5 ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ¬ 𝑞 = 𝑝 → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐 ) ∧ 𝑝 ∈ HAtoms ) → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ⊢ 𝐴 ∈ Cℋ
2 mdsymlem1.2 ⊢ 𝐵 ∈ Cℋ
3 mdsymlem1.3 ⊢ 𝐶 = ( 𝐴 ∨ℋ 𝑝 )
4 df-ne ⊢ ( 𝑞 ≠ 𝑝 ↔ ¬ 𝑞 = 𝑝 )
5 atnemeq0 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( 𝑞 ≠ 𝑝 ↔ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) )
6 4 5 bitr3id ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ¬ 𝑞 = 𝑝 ↔ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) )
7 6 anbi2d ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ¬ 𝑞 = 𝑝 ) ↔ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) ) )
8 7 3adant3 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ¬ 𝑞 = 𝑝 ) ↔ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) ) )
9 atelch ⊢ ( 𝑞 ∈ HAtoms → 𝑞 ∈ Cℋ )
10 atexch ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) )
11 9 10 syl3an1 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ∩ 𝑝 ) = 0ℋ ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) )
12 8 11 sylbid ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ¬ 𝑞 = 𝑝 ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) )
13 12 expd ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( ¬ 𝑞 = 𝑝 → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) )
14 13 3com23 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( ¬ 𝑞 = 𝑝 → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) )
15 14 3expa ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑝 ∈ HAtoms ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( ¬ 𝑞 = 𝑝 → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) )
16 15 adantrl ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( ¬ 𝑞 = 𝑝 → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) )
17 16 adantrd ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ¬ 𝑞 = 𝑝 → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) )
18 17 imp32 ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) )
19 18 adantrl ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) )
20 19 adantrr ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) )
21 simplrl ⊢ ( ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) → 𝑞 ⊆ 𝐴 )
22 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
23 22 anim1i ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑐 ∈ Cℋ ) → ( 𝑝 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) )
24 23 ancoms ⊢ ( ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) → ( 𝑝 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) )
25 chub2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) → 𝐴 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
26 1 25 mpan ⊢ ( 𝑐 ∈ Cℋ → 𝐴 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
27 sstr ⊢ ( ( 𝑞 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) → 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
28 26 27 sylan2 ⊢ ( ( 𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ ) → 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
29 chub1 ⊢ ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → 𝑐 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
30 1 29 mpan2 ⊢ ( 𝑐 ∈ Cℋ → 𝑐 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
31 sstr ⊢ ( ( 𝑝 ⊆ 𝑐 ∧ 𝑐 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) → 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
32 30 31 sylan2 ⊢ ( ( 𝑝 ⊆ 𝑐 ∧ 𝑐 ∈ Cℋ ) → 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
33 28 32 anim12i ⊢ ( ( ( 𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑝 ⊆ 𝑐 ∧ 𝑐 ∈ Cℋ ) ) → ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
34 33 anandirs ⊢ ( ( ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ∧ 𝑐 ∈ Cℋ ) → ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
35 34 ancoms ⊢ ( ( 𝑐 ∈ Cℋ ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) → ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
36 35 adantll ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) → ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
37 chjcl ⊢ ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑐 ∨ℋ 𝐴 ) ∈ Cℋ )
38 1 37 mpan2 ⊢ ( 𝑐 ∈ Cℋ → ( 𝑐 ∨ℋ 𝐴 ) ∈ Cℋ )
39 chlub ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ∧ ( 𝑐 ∨ℋ 𝐴 ) ∈ Cℋ ) → ( ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) ↔ ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
40 38 39 syl3an3 ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) → ( ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) ↔ ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
41 40 3expa ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) → ( ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) ↔ ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
42 41 adantr ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) → ( ( 𝑞 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ∧ 𝑝 ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) ↔ ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) ) )
43 36 42 mpbid ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) → ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
44 43 adantrl ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝐴 ⊆ 𝑐 ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) ) → ( 𝑞 ∨ℋ 𝑝 ) ⊆ ( 𝑐 ∨ℋ 𝐴 ) )
45 chlejb2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) → ( 𝐴 ⊆ 𝑐 ↔ ( 𝑐 ∨ℋ 𝐴 ) = 𝑐 ) )
46 1 45 mpan ⊢ ( 𝑐 ∈ Cℋ → ( 𝐴 ⊆ 𝑐 ↔ ( 𝑐 ∨ℋ 𝐴 ) = 𝑐 ) )
47 46 biimpa ⊢ ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐 ) → ( 𝑐 ∨ℋ 𝐴 ) = 𝑐 )
48 47 ad2ant2lr ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝐴 ⊆ 𝑐 ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) ) → ( 𝑐 ∨ℋ 𝐴 ) = 𝑐 )
49 44 48 sseqtrd ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝐴 ⊆ 𝑐 ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐 ) ) ) → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 )
50 49 exp45 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) → ( 𝐴 ⊆ 𝑐 → ( 𝑞 ⊆ 𝐴 → ( 𝑝 ⊆ 𝑐 → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 ) ) ) )
51 50 anasss ⊢ ( ( 𝑞 ∈ Cℋ ∧ ( 𝑝 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) ) → ( 𝐴 ⊆ 𝑐 → ( 𝑞 ⊆ 𝐴 → ( 𝑝 ⊆ 𝑐 → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 ) ) ) )
52 9 24 51 syl2an ⊢ ( ( 𝑞 ∈ HAtoms ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝐴 ⊆ 𝑐 → ( 𝑞 ⊆ 𝐴 → ( 𝑝 ⊆ 𝑐 → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 ) ) ) )
53 52 adantlr ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝐴 ⊆ 𝑐 → ( 𝑞 ⊆ 𝐴 → ( 𝑝 ⊆ 𝑐 → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 ) ) ) )
54 21 53 syl7 ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝐴 ⊆ 𝑐 → ( ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( 𝑝 ⊆ 𝑐 → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 ) ) ) )
55 54 imp44 ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → ( 𝑞 ∨ℋ 𝑝 ) ⊆ 𝑐 )
56 20 55 sstrd ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → 𝑟 ⊆ 𝑐 )
57 simplrr ⊢ ( ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) → 𝑟 ⊆ 𝐵 )
58 57 ad2antlr ⊢ ( ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) → 𝑟 ⊆ 𝐵 )
59 58 adantl ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → 𝑟 ⊆ 𝐵 )
60 56 59 ssind ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) )
61 atelch ⊢ ( 𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
62 9 61 anim12i ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) )
63 chincl ⊢ ( ( 𝑐 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑐 ∩ 𝐵 ) ∈ Cℋ )
64 2 63 mpan2 ⊢ ( 𝑐 ∈ Cℋ → ( 𝑐 ∩ 𝐵 ) ∈ Cℋ )
65 chlej1 ⊢ ( ( ( 𝑟 ∈ Cℋ ∧ ( 𝑐 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) )
66 65 ex ⊢ ( ( 𝑟 ∈ Cℋ ∧ ( 𝑐 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ) )
67 64 66 syl3an2 ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ) )
68 67 3comr ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ) )
69 68 3expa ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ) )
70 69 adantr ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ) )
71 chlej2 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ ( 𝑐 ∩ 𝐵 ) ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
72 1 71 mp3anl2 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ ( 𝑐 ∩ 𝐵 ) ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
73 64 72 sylanl2 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
74 73 adantllr ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
75 sstr2 ⊢ ( ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) → ( ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
76 74 75 syl5com ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) → ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
77 chjcom ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) → ( 𝑞 ∨ℋ 𝑟 ) = ( 𝑟 ∨ℋ 𝑞 ) )
78 77 ad2antrr ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( 𝑞 ∨ℋ 𝑟 ) = ( 𝑟 ∨ℋ 𝑞 ) )
79 78 sseq1d ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ↔ ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
80 76 79 sylibrd ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( ( 𝑟 ∨ℋ 𝑞 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝑞 ) → ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
81 70 80 syld ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ 𝑞 ⊆ 𝐴 ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
82 81 adantrl ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ 𝑞 ⊆ 𝐴 ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
83 sstr2 ⊢ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
84 83 ad2antrl ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ 𝑞 ⊆ 𝐴 ) ) → ( ( 𝑞 ∨ℋ 𝑟 ) ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
85 82 84 syld ⊢ ( ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) ∧ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ 𝑞 ⊆ 𝐴 ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
86 85 exp32 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ) ∧ 𝑐 ∈ Cℋ ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( 𝑞 ⊆ 𝐴 → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) )
87 62 86 sylan ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑐 ∈ Cℋ ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( 𝑞 ⊆ 𝐴 → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) )
88 87 adantrr ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) → ( 𝑞 ⊆ 𝐴 → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) )
89 88 imp31 ⊢ ( ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ∧ 𝑞 ⊆ 𝐴 ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
90 89 adantrr ⊢ ( ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
91 90 anasss ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
92 91 adantrr ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
93 92 adantrl ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
94 93 adantrr ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → ( 𝑟 ⊆ ( 𝑐 ∩ 𝐵 ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) )
95 60 94 mpd ⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) ∧ ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) ∧ 𝑝 ⊆ 𝑐 ) ) → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
96 95 exp32 ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( ( 𝐴 ⊆ 𝑐 ∧ ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ∧ ¬ 𝑞 = 𝑝 ) ) → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) )
97 96 exp4d ⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑐 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ) → ( 𝐴 ⊆ 𝑐 → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ¬ 𝑞 = 𝑝 → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) )
98 97 exp32 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑐 ∈ Cℋ → ( 𝑝 ∈ HAtoms → ( 𝐴 ⊆ 𝑐 → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ¬ 𝑞 = 𝑝 → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) ) ) )
99 98 com34 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑐 ∈ Cℋ → ( 𝐴 ⊆ 𝑐 → ( 𝑝 ∈ HAtoms → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ¬ 𝑞 = 𝑝 → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) ) ) )
100 99 imp4c ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐 ) ∧ 𝑝 ∈ HAtoms ) → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ¬ 𝑞 = 𝑝 → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) )
101 100 com24 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ¬ 𝑞 = 𝑝 → ( ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) → ( ( ( 𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐 ) ∧ 𝑝 ∈ HAtoms ) → ( 𝑝 ⊆ 𝑐 → 𝑝 ⊆ ( ( 𝑐 ∩ 𝐵 ) ∨ℋ 𝐴 ) ) ) ) ) )