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