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 syl5ibr ( 𝐵 = 𝐶 → ( ( 𝐶 ∈ 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 syl5ib ( ( 𝐵 ∈ 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 syl5bi ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ ( 𝐵 = 𝐶𝐶𝐴 ) → ( 𝐵 ⊆ ( 𝐴 𝐶 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴𝐵 ⊆ ( 𝐶 𝑥 ) ) ) ) )
92 42 91 syl7 ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ¬ ( 𝐵 = 𝐶𝐶𝐴 ) → ( ( 𝐴 ≠ 0𝐵 ⊆ ( 𝐴 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴𝐵 ⊆ ( 𝐶 𝑥 ) ) ) ) )
93 19 41 92 ecase3d ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0𝐵 ⊆ ( 𝐴 𝐶 ) ) → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴𝐵 ⊆ ( 𝐶 𝑥 ) ) ) )