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