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∈HAtomsx⊆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 imbitrid ⊢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 imbitrid ⊢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 eqtrid ⊢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∈HAtomsx⊆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