This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ Cℋ
Assertion atcvat3i ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ HAtoms ) )

Proof

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