This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atcvat4i

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of PtakPulmannova p. 68. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atcvat3.1 ⊢ 𝐴 ∈ Cℋ
Assertion atcvat4i ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 atcvat3.1 ⊢ 𝐴 ∈ Cℋ
2 1 hatomici ⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )
3 atelch ⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ )
4 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
5 chub1 ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝐶 ⊆ ( 𝐶 ∨ℋ 𝑥 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → 𝐶 ⊆ ( 𝐶 ∨ℋ 𝑥 ) )
7 sseq1 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ↔ 𝐶 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
8 6 7 imbitrrid ⊢ ( 𝐵 = 𝐶 → ( ( 𝐶 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
9 8 expd ⊢ ( 𝐵 = 𝐶 → ( 𝐶 ∈ HAtoms → ( 𝑥 ∈ HAtoms → 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )
10 9 impcom ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( 𝑥 ∈ HAtoms → 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
11 10 anim2d ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )
12 11 expcomd ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( 𝑥 ∈ HAtoms → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
13 12 reximdvai ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )
14 2 13 syl5 ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )
15 14 ex ⊢ ( 𝐶 ∈ HAtoms → ( 𝐵 = 𝐶 → ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
16 15 a1i ⊢ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ( 𝐶 ∈ HAtoms → ( 𝐵 = 𝐶 → ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) ) )
17 16 com4l ⊢ ( 𝐶 ∈ HAtoms → ( 𝐵 = 𝐶 → ( 𝐴 ≠ 0ℋ → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) ) )
18 17 imp4a ⊢ ( 𝐶 ∈ HAtoms → ( 𝐵 = 𝐶 → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
19 18 adantl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 = 𝐶 → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
20 atelch ⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
21 chlejb2 ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐶 ) = 𝐴 ) )
22 1 21 mpan2 ⊢ ( 𝐶 ∈ Cℋ → ( 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐶 ) = 𝐴 ) )
23 22 biimpa ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐴 ∨ℋ 𝐶 ) = 𝐴 )
24 23 sseq2d ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ↔ 𝐵 ⊆ 𝐴 ) )
25 24 biimpa ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → 𝐵 ⊆ 𝐴 )
26 25 expl ⊢ ( 𝐶 ∈ Cℋ → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → 𝐵 ⊆ 𝐴 ) )
27 26 adantl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → 𝐵 ⊆ 𝐴 ) )
28 chub2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) )
29 27 28 jctird ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) )
30 20 3 29 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) )
31 simpl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → 𝐵 ∈ HAtoms )
32 30 31 jctild ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐵 ∈ HAtoms ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) ) )
33 32 impl ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐵 ∈ HAtoms ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) )
34 sseq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
35 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 ∨ℋ 𝑥 ) = ( 𝐶 ∨ℋ 𝐵 ) )
36 35 sseq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ↔ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) )
37 34 36 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) )
38 37 rspcev ⊢ ( ( 𝐵 ∈ HAtoms ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝐵 ) ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
39 33 38 syl ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
40 39 adantrl ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
41 40 exp31 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
42 simpr ⊢ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) )
43 ioran ⊢ ( ¬ ( 𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴 ) ↔ ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) )
44 1 atcvat3i ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ) )
45 3 ad2antlr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → 𝐶 ∈ Cℋ )
46 44 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms )
47 simpll ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → 𝐵 ∈ HAtoms )
48 45 46 47 3jca ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) )
49 inss2 ⊢ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ ( 𝐵 ∨ℋ 𝐶 )
50 chjcom ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 ) )
51 20 3 50 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 ) )
52 49 51 sseqtrid ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ ( 𝐶 ∨ℋ 𝐵 ) )
53 52 adantr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ ( 𝐶 ∨ℋ 𝐵 ) )
54 atnssm0 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ HAtoms ) → ( ¬ 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 0ℋ ) )
55 1 54 mpan ⊢ ( 𝐶 ∈ HAtoms → ( ¬ 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 0ℋ ) )
56 55 adantl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 0ℋ ) )
57 inss1 ⊢ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴
58 sslin ⊢ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ ( 𝐶 ∩ 𝐴 ) )
59 57 58 ax-mp ⊢ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ ( 𝐶 ∩ 𝐴 )
60 incom ⊢ ( 𝐶 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐶 )
61 59 60 sseqtri ⊢ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ ( 𝐴 ∩ 𝐶 )
62 sseq2 ⊢ ( ( 𝐴 ∩ 𝐶 ) = 0ℋ → ( ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ 0ℋ ) )
63 61 62 mpbii ⊢ ( ( 𝐴 ∩ 𝐶 ) = 0ℋ → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ 0ℋ )
64 simpr ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐶 ∈ Cℋ )
65 chjcl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ )
66 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ Cℋ )
67 1 65 66 sylancr ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ Cℋ )
68 chincl ⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ Cℋ ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ∈ Cℋ )
69 64 67 68 syl2anc ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ∈ Cℋ )
70 20 3 69 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ∈ Cℋ )
71 chle0 ⊢ ( ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ∈ Cℋ → ( ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ 0ℋ ↔ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) )
72 70 71 syl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ⊆ 0ℋ ↔ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) )
73 63 72 imbitrid ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐶 ) = 0ℋ → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) )
74 56 73 sylbid ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ 𝐶 ⊆ 𝐴 → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) )
75 74 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ¬ 𝐶 ⊆ 𝐴 ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ )
76 75 adantrl ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ )
77 76 adantrr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ )
78 53 77 jca ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ ( 𝐶 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) )
79 atexch ⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ ( 𝐶 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = 0ℋ ) → 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) )
80 48 78 79 sylc ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) )
81 80 57 jctil ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) )
82 81 ex ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) ) )
83 44 82 jcad ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ∧ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) ) ) )
84 sseq1 ⊢ ( 𝑥 = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ) )
85 oveq2 ⊢ ( 𝑥 = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐶 ∨ℋ 𝑥 ) = ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) )
86 85 sseq2d ⊢ ( 𝑥 = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ↔ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) )
87 84 86 anbi12d ⊢ ( 𝑥 = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ↔ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) ) )
88 87 rspcev ⊢ ( ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ∧ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) )
89 83 88 syl6 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )
90 89 expd ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
91 43 90 biimtrid ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ ( 𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴 ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
92 42 91 syl7 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ ( 𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴 ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) ) )
93 19 41 92 ecase3d ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ ( 𝐶 ∨ℋ 𝑥 ) ) ) )