Metamath Proof Explorer

Theorem dmdbr5ati

Description: Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ⊢A∈Cℋ
sumdmdi.2 ⊢B∈Cℋ
Assertion dmdbr5ati ⊢A𝑀ℋ*B↔∀x∈HAtomsx⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢A∈Cℋ
2 sumdmdi.2 ⊢B∈Cℋ
3 dmdi4 ⊢A∈Cℋ∧B∈Cℋ∧x∈Cℋ→A𝑀ℋ*B→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
4 1 2 3 mp3an12 ⊢x∈Cℋ→A𝑀ℋ*B→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
5 atelch ⊢x∈HAtoms→x∈Cℋ
6 4 5 syl11 ⊢A𝑀ℋ*B→x∈HAtoms→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
7 6 a1dd ⊢A𝑀ℋ*B→x∈HAtoms→x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
8 7 ralrimiv ⊢A𝑀ℋ*B→∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
9 chjcom ⊢B∈Cℋ∧x∈Cℋ→B∨ℋx=x∨ℋB
10 2 5 9 sylancr ⊢x∈HAtoms→B∨ℋx=x∨ℋB
11 10 ineq1d ⊢x∈HAtoms→B∨ℋx∩B∨ℋA=x∨ℋB∩B∨ℋA
12 1 2 chjcomi ⊢A∨ℋB=B∨ℋA
13 12 ineq2i ⊢x∨ℋB∩A∨ℋB=x∨ℋB∩B∨ℋA
14 11 13 eqtr4di ⊢x∈HAtoms→B∨ℋx∩B∨ℋA=x∨ℋB∩A∨ℋB
15 14 adantr ⊢x∈HAtoms∧¬x⊆A∨ℋB→B∨ℋx∩B∨ℋA=x∨ℋB∩A∨ℋB
16 12 sseq2i ⊢x⊆A∨ℋB↔x⊆B∨ℋA
17 16 notbii ⊢¬x⊆A∨ℋB↔¬x⊆B∨ℋA
18 2 1 atabs2i ⊢x∈HAtoms→¬x⊆B∨ℋA→B∨ℋx∩B∨ℋA=B
19 18 imp ⊢x∈HAtoms∧¬x⊆B∨ℋA→B∨ℋx∩B∨ℋA=B
20 17 19 sylan2b ⊢x∈HAtoms∧¬x⊆A∨ℋB→B∨ℋx∩B∨ℋA=B
21 15 20 eqtr3d ⊢x∈HAtoms∧¬x⊆A∨ℋB→x∨ℋB∩A∨ℋB=B
22 chjcl ⊢x∈Cℋ∧B∈Cℋ→x∨ℋB∈Cℋ
23 5 2 22 sylancl ⊢x∈HAtoms→x∨ℋB∈Cℋ
24 chincl ⊢x∨ℋB∈Cℋ∧A∈Cℋ→x∨ℋB∩A∈Cℋ
25 23 1 24 sylancl ⊢x∈HAtoms→x∨ℋB∩A∈Cℋ
26 chub2 ⊢B∈Cℋ∧x∨ℋB∩A∈Cℋ→B⊆x∨ℋB∩A∨ℋB
27 2 25 26 sylancr ⊢x∈HAtoms→B⊆x∨ℋB∩A∨ℋB
28 27 adantr ⊢x∈HAtoms∧¬x⊆A∨ℋB→B⊆x∨ℋB∩A∨ℋB
29 21 28 eqsstrd ⊢x∈HAtoms∧¬x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
30 29 ex ⊢x∈HAtoms→¬x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
31 30 biantrud ⊢x∈HAtoms→x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB∧¬x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
32 pm4.83 ⊢x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB∧¬x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
33 31 32 bitrdi ⊢x∈HAtoms→x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
34 33 ralbiia ⊢∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔∀x∈HAtomsx∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
35 1 2 sumdmdlem2 ⊢∀x∈HAtomsx∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB→A+ℋB=A∨ℋB
36 34 35 sylbi ⊢∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB→A+ℋB=A∨ℋB
37 1 2 sumdmdi ⊢A+ℋB=A∨ℋB↔A𝑀ℋ*B
38 36 37 sylib ⊢∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB→A𝑀ℋ*B
39 8 38 impbii ⊢A𝑀ℋ*B↔∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB
40 2 1 chub2i ⊢B⊆A∨ℋB
41 40 biantru ⊢x⊆A∨ℋB↔x⊆A∨ℋB∧B⊆A∨ℋB
42 1 2 chjcli ⊢A∨ℋB∈Cℋ
43 chlub ⊢x∈Cℋ∧B∈Cℋ∧A∨ℋB∈Cℋ→x⊆A∨ℋB∧B⊆A∨ℋB↔x∨ℋB⊆A∨ℋB
44 2 42 43 mp3an23 ⊢x∈Cℋ→x⊆A∨ℋB∧B⊆A∨ℋB↔x∨ℋB⊆A∨ℋB
45 41 44 bitrid ⊢x∈Cℋ→x⊆A∨ℋB↔x∨ℋB⊆A∨ℋB
46 ssid ⊢x∨ℋB⊆x∨ℋB
47 46 biantrur ⊢x∨ℋB⊆A∨ℋB↔x∨ℋB⊆x∨ℋB∧x∨ℋB⊆A∨ℋB
48 ssin ⊢x∨ℋB⊆x∨ℋB∧x∨ℋB⊆A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
49 47 48 bitri ⊢x∨ℋB⊆A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
50 45 49 bitrdi ⊢x∈Cℋ→x⊆A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
51 50 biimpa ⊢x∈Cℋ∧x⊆A∨ℋB→x∨ℋB⊆x∨ℋB∩A∨ℋB
52 inss1 ⊢x∨ℋB∩A∨ℋB⊆x∨ℋB
53 51 52 jctil ⊢x∈Cℋ∧x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∧x∨ℋB⊆x∨ℋB∩A∨ℋB
54 eqss ⊢x∨ℋB∩A∨ℋB=x∨ℋB↔x∨ℋB∩A∨ℋB⊆x∨ℋB∧x∨ℋB⊆x∨ℋB∩A∨ℋB
55 53 54 sylibr ⊢x∈Cℋ∧x⊆A∨ℋB→x∨ℋB∩A∨ℋB=x∨ℋB
56 55 sseq1d ⊢x∈Cℋ∧x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
57 2 22 mpan2 ⊢x∈Cℋ→x∨ℋB∈Cℋ
58 57 1 24 sylancl ⊢x∈Cℋ→x∨ℋB∩A∈Cℋ
59 2 58 26 sylancr ⊢x∈Cℋ→B⊆x∨ℋB∩A∨ℋB
60 59 biantrud ⊢x∈Cℋ→x⊆x∨ℋB∩A∨ℋB↔x⊆x∨ℋB∩A∨ℋB∧B⊆x∨ℋB∩A∨ℋB
61 chjcl ⊢x∨ℋB∩A∈Cℋ∧B∈Cℋ→x∨ℋB∩A∨ℋB∈Cℋ
62 58 2 61 sylancl ⊢x∈Cℋ→x∨ℋB∩A∨ℋB∈Cℋ
63 chlub ⊢x∈Cℋ∧B∈Cℋ∧x∨ℋB∩A∨ℋB∈Cℋ→x⊆x∨ℋB∩A∨ℋB∧B⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
64 2 63 mp3an2 ⊢x∈Cℋ∧x∨ℋB∩A∨ℋB∈Cℋ→x⊆x∨ℋB∩A∨ℋB∧B⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
65 62 64 mpdan ⊢x∈Cℋ→x⊆x∨ℋB∩A∨ℋB∧B⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
66 60 65 bitrd ⊢x∈Cℋ→x⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
67 66 adantr ⊢x∈Cℋ∧x⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB↔x∨ℋB⊆x∨ℋB∩A∨ℋB
68 56 67 bitr4d ⊢x∈Cℋ∧x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x⊆x∨ℋB∩A∨ℋB
69 68 pm5.74da ⊢x∈Cℋ→x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB
70 5 69 syl ⊢x∈HAtoms→x⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔x⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB
71 70 ralbiia ⊢∀x∈HAtomsx⊆A∨ℋB→x∨ℋB∩A∨ℋB⊆x∨ℋB∩A∨ℋB↔∀x∈HAtomsx⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB
72 39 71 bitri ⊢A𝑀ℋ*B↔∀x∈HAtomsx⊆A∨ℋB→x⊆x∨ℋB∩A∨ℋB