Metamath Proof Explorer

Theorem atcvatlem

Description: Lemma for atcvati . (Contributed by NM, 27-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 ⊢ 𝐴 ∈ Cℋ
Assertion atcvatlem ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) )

Proof

Step Hyp Ref Expression
1 atoml.1 ⊢ 𝐴 ∈ Cℋ
2 1 hatomici ⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )
3 nssne2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) → 𝑥 ≠ 𝐵 )
4 3 adantrl ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝑥 ≠ 𝐵 )
5 atnemeq0 ⊢ ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝑥 ≠ 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) = 0ℋ ) )
6 4 5 syl5ib ⊢ ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → ( 𝑥 ∩ 𝐵 ) = 0ℋ ) )
7 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
8 cvp ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ∩ 𝐵 ) = 0ℋ ↔ 𝑥 ⋖ℋ ( 𝑥 ∨ℋ 𝐵 ) ) )
9 atelch ⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
10 chjcom ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝑥 ) )
11 9 10 sylan2 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝑥 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝑥 ) )
12 11 breq2d ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝑥 ⋖ℋ ( 𝑥 ∨ℋ 𝐵 ) ↔ 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
13 8 12 bitrd ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ∩ 𝐵 ) = 0ℋ ↔ 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
14 7 13 sylan ⊢ ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ∩ 𝐵 ) = 0ℋ ↔ 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
15 6 14 sylibd ⊢ ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
16 15 ancoms ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
17 16 adantlr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ) )
18 17 imp ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) )
19 chub1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
20 9 7 19 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
21 20 3adant3 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
22 21 adantr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
23 pssss ⊢ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
24 sstr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
25 23 24 sylan2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
26 25 adantlr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
27 26 adantl ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
28 incom ⊢ ( 𝐵 ∩ 𝑥 ) = ( 𝑥 ∩ 𝐵 )
29 3 5 syl5ib ⊢ ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∩ 𝐵 ) = 0ℋ ) )
30 29 ancoms ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∩ 𝐵 ) = 0ℋ ) )
31 30 3adant3 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∩ 𝐵 ) = 0ℋ ) )
32 31 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → ( 𝑥 ∩ 𝐵 ) = 0ℋ )
33 28 32 eqtrid ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → ( 𝐵 ∩ 𝑥 ) = 0ℋ )
34 33 adantrr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ∩ 𝑥 ) = 0ℋ )
35 atexch ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ ( 𝐵 ∩ 𝑥 ) = 0ℋ ) → 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
36 9 35 syl3an1 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ ( 𝐵 ∩ 𝑥 ) = 0ℋ ) → 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
37 36 adantr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ( 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ ( 𝐵 ∩ 𝑥 ) = 0ℋ ) → 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
38 27 34 37 mp2and ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
39 atelch ⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ )
40 simp1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ∈ Cℋ )
41 simp3 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐶 ∈ Cℋ )
42 chjcl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ )
43 42 3adant3 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ )
44 40 41 43 3jca ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) )
45 9 7 39 44 syl3an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) )
46 chlub ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) ↔ ( 𝐵 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
47 45 46 syl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) ↔ ( 𝐵 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
48 47 adantr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐶 ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) ↔ ( 𝐵 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝑥 ) ) )
49 22 38 48 mpbi2and ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝑥 ) )
50 chub1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
51 50 3adant2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
52 51 26 anim12i ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) )
53 chjcl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ )
54 53 3adant2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ )
55 chlub ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) ↔ ( 𝐵 ∨ℋ 𝑥 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) )
56 54 55 syld3an3 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) ↔ ( 𝐵 ∨ℋ 𝑥 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) )
57 56 adantr ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ( 𝐵 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ∧ 𝑥 ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) ↔ ( 𝐵 ∨ℋ 𝑥 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) )
58 52 57 mpbid ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ∨ℋ 𝑥 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
59 9 7 39 58 syl3anl ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ∨ℋ 𝑥 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
60 49 59 eqssd ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐵 ∨ℋ 𝑥 ) )
61 60 anassrs ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐵 ∨ℋ 𝑥 ) )
62 61 psseq2d ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) )
63 62 ex ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) ) )
64 63 ibd ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) )
65 64 exp32 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( ¬ 𝐵 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) ) ) )
66 65 3expa ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ 𝐶 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( ¬ 𝐵 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) ) ) )
67 66 an32s ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( ¬ 𝐵 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) ) ) )
68 67 com34 ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) ) ) )
69 68 imp45 ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) )
70 simpr ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝑥 ∈ Cℋ )
71 70 42 jca ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) )
72 9 7 71 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) )
73 cvnbtwn3 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) ) )
74 1 73 mp3an3 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) ) )
75 74 exp4a ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) → ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) → 𝐴 = 𝑥 ) ) ) )
76 75 com23 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) → 𝐴 = 𝑥 ) ) ) )
77 76 imp4a ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) ) )
78 72 77 syl ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) ) )
79 78 adantlr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) ) )
80 79 imp ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) )
81 80 adantrr ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → ( ( 𝑥 ⋖ℋ ( 𝐵 ∨ℋ 𝑥 ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝑥 ) ) → 𝐴 = 𝑥 ) )
82 18 69 81 mp2and ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → 𝐴 = 𝑥 )
83 82 eleq1d ⊢ ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → ( 𝐴 ∈ HAtoms ↔ 𝑥 ∈ HAtoms ) )
84 83 biimprcd ⊢ ( 𝑥 ∈ HAtoms → ( ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) ) → 𝐴 ∈ HAtoms ) )
85 84 exp4c ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝐴 ∈ HAtoms ) ) ) )
86 85 pm2.43b ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝐴 ∈ HAtoms ) ) )
87 86 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ∧ ¬ 𝐵 ⊆ 𝐴 ) ) → 𝐴 ∈ HAtoms ) )
88 87 exp4d ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) ) )
89 88 rexlimdva ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) ) )
90 2 89 syl5 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ≠ 0ℋ → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) ) )
91 90 imp32 ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) )