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 ⊢ A ∈ C ℋ
Assertion atcvat4i ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ≠ 0 ℋ ∧ B ⊆ A ∨ ℋ C → ∃ x ∈ HAtoms x ⊆ A ∧ B ⊆ C ∨ ℋ x

Proof

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