Metamath Proof Explorer

Theorem atcvat3i

Description: A condition implying that a certain lattice element is an atom. Part of 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 atcvat3i ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms

Proof

Step Hyp Ref Expression
1 atcvat3.1 ⊢ A ∈ C ℋ
2 chcv1 ⊢ A ∈ C ℋ ∧ C ∈ HAtoms → ¬ C ⊆ A ↔ A ⋖ ℋ A ∨ ℋ C
3 1 2 mpan ⊢ C ∈ HAtoms → ¬ C ⊆ A ↔ A ⋖ ℋ A ∨ ℋ C
4 3 biimpa ⊢ C ∈ HAtoms ∧ ¬ C ⊆ A → A ⋖ ℋ A ∨ ℋ C
5 4 ad2ant2lr ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ⋖ ℋ A ∨ ℋ C
6 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
7 atelch ⊢ C ∈ HAtoms → C ∈ C ℋ
8 6 7 anim12i ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → B ∈ C ℋ ∧ C ∈ C ℋ
9 chjcom ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → B ∨ ℋ C = C ∨ ℋ B
10 9 oveq2d ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ B ∨ ℋ C = A ∨ ℋ C ∨ ℋ B
11 chjass ⊢ A ∈ C ℋ ∧ C ∈ C ℋ ∧ B ∈ C ℋ → A ∨ ℋ C ∨ ℋ B = A ∨ ℋ C ∨ ℋ B
12 1 11 mp3an1 ⊢ C ∈ C ℋ ∧ B ∈ C ℋ → A ∨ ℋ C ∨ ℋ B = A ∨ ℋ C ∨ ℋ B
13 12 ancoms ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ C ∨ ℋ B = A ∨ ℋ C ∨ ℋ B
14 10 13 eqtr4d ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ B ∨ ℋ C = A ∨ ℋ C ∨ ℋ B
15 14 adantr ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ B ∨ ℋ C = A ∨ ℋ C ∨ ℋ B
16 simpl ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → B ∈ C ℋ
17 chjcl ⊢ A ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ C ∈ C ℋ
18 1 17 mpan ⊢ C ∈ C ℋ → A ∨ ℋ C ∈ C ℋ
19 18 adantl ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ C ∈ C ℋ
20 chlej2 ⊢ B ∈ C ℋ ∧ A ∨ ℋ C ∈ C ℋ ∧ A ∨ ℋ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ C ∨ ℋ B ⊆ A ∨ ℋ C ∨ ℋ A ∨ ℋ C
21 20 ex ⊢ B ∈ C ℋ ∧ A ∨ ℋ C ∈ C ℋ ∧ A ∨ ℋ C ∈ C ℋ → B ⊆ A ∨ ℋ C → A ∨ ℋ C ∨ ℋ B ⊆ A ∨ ℋ C ∨ ℋ A ∨ ℋ C
22 16 19 19 21 syl3anc ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → B ⊆ A ∨ ℋ C → A ∨ ℋ C ∨ ℋ B ⊆ A ∨ ℋ C ∨ ℋ A ∨ ℋ C
23 22 imp ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ C ∨ ℋ B ⊆ A ∨ ℋ C ∨ ℋ A ∨ ℋ C
24 15 23 eqsstrd ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ B ∨ ℋ C ⊆ A ∨ ℋ C ∨ ℋ A ∨ ℋ C
25 chjidm ⊢ A ∨ ℋ C ∈ C ℋ → A ∨ ℋ C ∨ ℋ A ∨ ℋ C = A ∨ ℋ C
26 18 25 syl ⊢ C ∈ C ℋ → A ∨ ℋ C ∨ ℋ A ∨ ℋ C = A ∨ ℋ C
27 26 ad2antlr ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ C ∨ ℋ A ∨ ℋ C = A ∨ ℋ C
28 24 27 sseqtrd ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ B ∨ ℋ C ⊆ A ∨ ℋ C
29 simpr ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → C ∈ C ℋ
30 chjcl ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → B ∨ ℋ C ∈ C ℋ
31 chub2 ⊢ C ∈ C ℋ ∧ B ∈ C ℋ → C ⊆ B ∨ ℋ C
32 31 ancoms ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → C ⊆ B ∨ ℋ C
33 chlej2 ⊢ C ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ ∧ A ∈ C ℋ ∧ C ⊆ B ∨ ℋ C → A ∨ ℋ C ⊆ A ∨ ℋ B ∨ ℋ C
34 1 33 mp3anl3 ⊢ C ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ ∧ C ⊆ B ∨ ℋ C → A ∨ ℋ C ⊆ A ∨ ℋ B ∨ ℋ C
35 29 30 32 34 syl21anc ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∨ ℋ C ⊆ A ∨ ℋ B ∨ ℋ C
36 35 adantr ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ C ⊆ A ∨ ℋ B ∨ ℋ C
37 28 36 eqssd ⊢ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ B ∨ ℋ C = A ∨ ℋ C
38 8 37 sylan ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ B ⊆ A ∨ ℋ C → A ∨ ℋ B ∨ ℋ C = A ∨ ℋ C
39 38 breq2d ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ B ⊆ A ∨ ℋ C → A ⋖ ℋ A ∨ ℋ B ∨ ℋ C ↔ A ⋖ ℋ A ∨ ℋ C
40 39 adantrl ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ⋖ ℋ A ∨ ℋ B ∨ ℋ C ↔ A ⋖ ℋ A ∨ ℋ C
41 5 40 mpbird ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ⋖ ℋ A ∨ ℋ B ∨ ℋ C
42 41 ex ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ⋖ ℋ A ∨ ℋ B ∨ ℋ C
43 30 1 jctil ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ
44 6 7 43 syl2an ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ
45 cvexch ⊢ A ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ → A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C ↔ A ⋖ ℋ A ∨ ℋ B ∨ ℋ C
46 44 45 syl ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C ↔ A ⋖ ℋ A ∨ ℋ B ∨ ℋ C
47 42 46 sylibrd ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C
48 47 adantr ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ B = C → ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C
49 chincl ⊢ A ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ → A ∩ B ∨ ℋ C ∈ C ℋ
50 1 30 49 sylancr ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → A ∩ B ∨ ℋ C ∈ C ℋ
51 6 7 50 syl2an ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ∩ B ∨ ℋ C ∈ C ℋ
52 simpl ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → B ∈ HAtoms
53 simpr ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → C ∈ HAtoms
54 atcvat2 ⊢ A ∩ B ∨ ℋ C ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms
55 51 52 53 54 syl3anc ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms
56 55 expdimp ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ B = C → A ∩ B ∨ ℋ C ⋖ ℋ B ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms
57 48 56 syld ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ ¬ B = C → ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms
58 57 exp4b ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C → ¬ C ⊆ A → B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms
59 58 imp4c ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ ¬ C ⊆ A ∧ B ⊆ A ∨ ℋ C → A ∩ B ∨ ℋ C ∈ HAtoms