Metamath Proof Explorer

Theorem atcvatlem

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

Ref Expression
Hypothesis atoml.1 ⊢ A ∈ C ℋ
Assertion atcvatlem ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ≠ 0 ℋ ∧ A ⊂ B ∨ ℋ C → ¬ B ⊆ A → A ∈ HAtoms

Proof

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