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∈HAtomsx⊆A∧B⊆C∨ℋx

Proof

Step Hyp Ref Expression
1 atcvat3.1 ⊢A∈Cℋ
2 1 hatomici ⊢A≠0ℋ→∃x∈HAtomsx⊆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 imbitrrid ⊢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∈HAtomsx⊆A→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
14 2 13 syl5 ⊢C∈HAtoms∧B=C→A≠0ℋ→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
15 14 ex ⊢C∈HAtoms→B=C→A≠0ℋ→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
16 15 a1i ⊢B⊆A∨ℋC→C∈HAtoms→B=C→A≠0ℋ→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
17 16 com4l ⊢C∈HAtoms→B=C→A≠0ℋ→B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
18 17 imp4a ⊢C∈HAtoms→B=C→A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
19 18 adantl ⊢B∈HAtoms∧C∈HAtoms→B=C→A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆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∈HAtomsx⊆A∧B⊆C∨ℋx
39 33 38 syl ⊢B∈HAtoms∧C∈HAtoms∧C⊆A∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
40 39 adantrl ⊢B∈HAtoms∧C∈HAtoms∧C⊆A∧A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
41 40 exp31 ⊢B∈HAtoms∧C∈HAtoms→C⊆A→A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆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 imbitrid ⊢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∈HAtomsx⊆A∧B⊆C∨ℋx
89 83 88 syl6 ⊢B∈HAtoms∧C∈HAtoms→¬B=C∧¬C⊆A∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
90 89 expd ⊢B∈HAtoms∧C∈HAtoms→¬B=C∧¬C⊆A→B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
91 43 90 biimtrid ⊢B∈HAtoms∧C∈HAtoms→¬B=C∨C⊆A→B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
92 42 91 syl7 ⊢B∈HAtoms∧C∈HAtoms→¬B=C∨C⊆A→A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx
93 19 41 92 ecase3d ⊢B∈HAtoms∧C∈HAtoms→A≠0ℋ∧B⊆A∨ℋC→∃x∈HAtomsx⊆A∧B⊆C∨ℋx