Metamath Proof Explorer

Theorem mdsymlem3

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 mdsymlem3 ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑟 ∈ HAtoms ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ⊢ 𝐴 ∈ Cℋ
2 mdsymlem1.2 ⊢ 𝐵 ∈ Cℋ
3 mdsymlem1.3 ⊢ 𝐶 = ( 𝐴 ∨ℋ 𝑝 )
4 ssin ⊢ ( ( 𝑟 ⊆ 𝐵 ∧ 𝑟 ⊆ 𝐶 ) ↔ 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) )
5 3 sseq2i ⊢ ( 𝑟 ⊆ 𝐶 ↔ 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) )
6 5 biimpi ⊢ ( 𝑟 ⊆ 𝐶 → 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) )
7 6 adantl ⊢ ( ( 𝑟 ⊆ 𝐵 ∧ 𝑟 ⊆ 𝐶 ) → 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) )
8 4 7 sylbir ⊢ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) → 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) )
9 1 atcvat4i ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
10 9 exp4b ⊢ ( 𝑟 ∈ HAtoms → ( 𝑝 ∈ HAtoms → ( 𝐴 ≠ 0ℋ → ( 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) ) ) )
11 10 com34 ⊢ ( 𝑟 ∈ HAtoms → ( 𝑝 ∈ HAtoms → ( 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) → ( 𝐴 ≠ 0ℋ → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) ) ) )
12 11 com23 ⊢ ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) → ( 𝑝 ∈ HAtoms → ( 𝐴 ≠ 0ℋ → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) ) ) )
13 12 imp4b ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝐴 ∨ℋ 𝑝 ) ) → ( ( 𝑝 ∈ HAtoms ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
14 8 13 sylan2 ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑝 ∈ HAtoms ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
15 14 adantrr ⊢ ( ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ( ( 𝑝 ∈ HAtoms ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
16 15 com12 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝐴 ≠ 0ℋ ) → ( ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
17 16 adantlr ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝐴 ≠ 0ℋ ) → ( ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
18 17 adantlr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) → ( ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
19 18 imp ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
20 nssne2 ⊢ ( ( 𝑞 ⊆ 𝐴 ∧ ¬ 𝑟 ⊆ 𝐴 ) → 𝑞 ≠ 𝑟 )
21 20 adantrl ⊢ ( ( 𝑞 ⊆ 𝐴 ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → 𝑞 ≠ 𝑟 )
22 atnemeq0 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑞 ≠ 𝑟 ↔ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) )
23 22 ancoms ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) → ( 𝑞 ≠ 𝑟 ↔ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) )
24 21 23 imbitrid ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) → ( ( 𝑞 ⊆ 𝐴 ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ( 𝑞 ∩ 𝑟 ) = 0ℋ ) )
25 24 adantll ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( ( 𝑞 ⊆ 𝐴 ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ( 𝑞 ∩ 𝑟 ) = 0ℋ ) )
26 25 adantr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( ( 𝑞 ⊆ 𝐴 ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ( 𝑞 ∩ 𝑟 ) = 0ℋ ) )
27 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
28 atelch ⊢ ( 𝑞 ∈ HAtoms → 𝑞 ∈ Cℋ )
29 chjcom ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
30 27 28 29 syl2an ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
31 30 adantlr ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
32 31 sseq2d ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ↔ 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) )
33 atexch ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ∧ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
34 28 33 syl3an1 ⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ∧ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
35 34 3com13 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ) → ( ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ∧ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
36 35 3expa ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ∧ ( 𝑞 ∩ 𝑟 ) = 0ℋ ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
37 36 expd ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) → ( ( 𝑞 ∩ 𝑟 ) = 0ℋ → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) )
38 32 37 sylbid ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( ( 𝑞 ∩ 𝑟 ) = 0ℋ → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) )
39 38 imp ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( ( 𝑞 ∩ 𝑟 ) = 0ℋ → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
40 26 39 syld ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( ( 𝑞 ⊆ 𝐴 ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
41 40 expd ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ 𝑞 ∈ HAtoms ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑞 ⊆ 𝐴 → ( ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) )
42 41 exp31 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑞 ∈ HAtoms → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑞 ⊆ 𝐴 → ( ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) ) ) )
43 42 com24 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( 𝑞 ⊆ 𝐴 → ( 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) → ( 𝑞 ∈ HAtoms → ( ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) ) ) )
44 43 impd ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑞 ∈ HAtoms → ( ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) ) )
45 44 com24 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) → ( ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) → ( 𝑞 ∈ HAtoms → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) ) ) )
46 45 imp4b ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ) ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
47 46 anasss ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ) )
48 simprl ⊢ ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑞 ⊆ 𝐴 )
49 48 a1i ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑞 ⊆ 𝐴 ) )
50 simpl ⊢ ( ( 𝑟 ⊆ 𝐵 ∧ 𝑟 ⊆ 𝐶 ) → 𝑟 ⊆ 𝐵 )
51 4 50 sylbir ⊢ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) → 𝑟 ⊆ 𝐵 )
52 51 ad2antrl ⊢ ( ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) → 𝑟 ⊆ 𝐵 )
53 52 adantl ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → 𝑟 ⊆ 𝐵 )
54 49 53 jctird ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) )
55 47 54 jcad ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( ( 𝑞 ∈ HAtoms ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) )
56 55 expd ⊢ ( ( 𝑝 ∈ HAtoms ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( 𝑞 ∈ HAtoms → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )
57 56 adantlr ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( 𝑞 ∈ HAtoms → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )
58 57 adantlr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( 𝑞 ∈ HAtoms → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )
59 58 adantlr ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( 𝑞 ∈ HAtoms → ( ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )
60 59 reximdvai ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ( ∃ 𝑞 ∈ HAtoms ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) )
61 19 60 mpd ⊢ ( ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) ∧ ( 𝑟 ∈ HAtoms ∧ ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) ) → ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) )
62 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑝 ) ∈ Cℋ )
63 1 62 mpan ⊢ ( 𝑝 ∈ Cℋ → ( 𝐴 ∨ℋ 𝑝 ) ∈ Cℋ )
64 3 63 eqeltrid ⊢ ( 𝑝 ∈ Cℋ → 𝐶 ∈ Cℋ )
65 chincl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∩ 𝐶 ) ∈ Cℋ )
66 2 64 65 sylancr ⊢ ( 𝑝 ∈ Cℋ → ( 𝐵 ∩ 𝐶 ) ∈ Cℋ )
67 27 66 syl ⊢ ( 𝑝 ∈ HAtoms → ( 𝐵 ∩ 𝐶 ) ∈ Cℋ )
68 chrelat2 ⊢ ( ( ( 𝐵 ∩ 𝐶 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ↔ ∃ 𝑟 ∈ HAtoms ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) )
69 67 1 68 sylancl ⊢ ( 𝑝 ∈ HAtoms → ( ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ↔ ∃ 𝑟 ∈ HAtoms ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) ) )
70 69 biimpa ⊢ ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) → ∃ 𝑟 ∈ HAtoms ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) )
71 70 ad2antrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑟 ∈ HAtoms ( 𝑟 ⊆ ( 𝐵 ∩ 𝐶 ) ∧ ¬ 𝑟 ⊆ 𝐴 ) )
72 61 71 reximddv ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ ¬ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐴 ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑟 ∈ HAtoms ∃ 𝑞 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) )