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 syl5eq ( ( ( 𝐵 ∈ 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 ) )