Metamath Proof Explorer

Theorem mdsymlem6

Description: Lemma for mdsymi . This is the converse direction of Lemma 4(i) of Maeda p. 168, and is based on the proof of Theorem 1(d) to (e) of Maeda p. 167. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢ A ∈ C ℋ
mdsymlem1.2 ⊢ B ∈ C ℋ
mdsymlem1.3 ⊢ C = A ∨ ℋ p
Assertion mdsymlem6 ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → B 𝑀 ℋ * A

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ⊢ A ∈ C ℋ
2 mdsymlem1.2 ⊢ B ∈ C ℋ
3 mdsymlem1.3 ⊢ C = A ∨ ℋ p
4 1 2 chjcomi ⊢ A ∨ ℋ B = B ∨ ℋ A
5 4 sseq2i ⊢ p ⊆ A ∨ ℋ B ↔ p ⊆ B ∨ ℋ A
6 5 anbi2i ⊢ p ⊆ c ∧ p ⊆ A ∨ ℋ B ↔ p ⊆ c ∧ p ⊆ B ∨ ℋ A
7 ssin ⊢ p ⊆ c ∧ p ⊆ B ∨ ℋ A ↔ p ⊆ c ∩ B ∨ ℋ A
8 6 7 bitri ⊢ p ⊆ c ∧ p ⊆ A ∨ ℋ B ↔ p ⊆ c ∩ B ∨ ℋ A
9 1 2 3 mdsymlem5 ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → ¬ q = p → p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
10 sseq1 ⊢ q = p → q ⊆ A ↔ p ⊆ A
11 chincl ⊢ c ∈ C ℋ ∧ B ∈ C ℋ → c ∩ B ∈ C ℋ
12 2 11 mpan2 ⊢ c ∈ C ℋ → c ∩ B ∈ C ℋ
13 chub2 ⊢ A ∈ C ℋ ∧ c ∩ B ∈ C ℋ → A ⊆ c ∩ B ∨ ℋ A
14 1 12 13 sylancr ⊢ c ∈ C ℋ → A ⊆ c ∩ B ∨ ℋ A
15 sstr2 ⊢ p ⊆ A → A ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
16 14 15 syl5 ⊢ p ⊆ A → c ∈ C ℋ → p ⊆ c ∩ B ∨ ℋ A
17 10 16 syl6bi ⊢ q = p → q ⊆ A → c ∈ C ℋ → p ⊆ c ∩ B ∨ ℋ A
18 17 impd ⊢ q = p → q ⊆ A ∧ c ∈ C ℋ → p ⊆ c ∩ B ∨ ℋ A
19 18 a1i ⊢ p ⊆ c → q = p → q ⊆ A ∧ c ∈ C ℋ → p ⊆ c ∩ B ∨ ℋ A
20 19 com13 ⊢ q ⊆ A ∧ c ∈ C ℋ → q = p → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
21 20 adantrr ⊢ q ⊆ A ∧ c ∈ C ℋ ∧ A ⊆ c → q = p → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
22 21 ad2ant2r ⊢ q ⊆ A ∧ r ⊆ B ∧ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → q = p → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
23 22 adantll ⊢ p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ∧ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → q = p → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
24 23 com12 ⊢ q = p → p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ∧ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
25 24 expd ⊢ q = p → p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
26 9 25 pm2.61d2 ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
27 26 rexlimivv ⊢ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
28 27 com12 ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
29 28 imim2d ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ A ∨ ℋ B → p ⊆ c → p ⊆ c ∩ B ∨ ℋ A
30 29 com34 ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ c → p ⊆ A ∨ ℋ B → p ⊆ c ∩ B ∨ ℋ A
31 30 imp4b ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms ∧ p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ c ∧ p ⊆ A ∨ ℋ B → p ⊆ c ∩ B ∨ ℋ A
32 8 31 syl5bir ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms ∧ p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
33 32 ex ⊢ c ∈ C ℋ ∧ A ⊆ c ∧ p ∈ HAtoms → p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
34 33 ralimdva ⊢ c ∈ C ℋ ∧ A ⊆ c → ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → ∀ p ∈ HAtoms p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
35 2 1 chjcli ⊢ B ∨ ℋ A ∈ C ℋ
36 chincl ⊢ c ∈ C ℋ ∧ B ∨ ℋ A ∈ C ℋ → c ∩ B ∨ ℋ A ∈ C ℋ
37 35 36 mpan2 ⊢ c ∈ C ℋ → c ∩ B ∨ ℋ A ∈ C ℋ
38 chjcl ⊢ c ∩ B ∈ C ℋ ∧ A ∈ C ℋ → c ∩ B ∨ ℋ A ∈ C ℋ
39 12 1 38 sylancl ⊢ c ∈ C ℋ → c ∩ B ∨ ℋ A ∈ C ℋ
40 chrelat3 ⊢ c ∩ B ∨ ℋ A ∈ C ℋ ∧ c ∩ B ∨ ℋ A ∈ C ℋ → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A ↔ ∀ p ∈ HAtoms p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
41 37 39 40 syl2anc ⊢ c ∈ C ℋ → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A ↔ ∀ p ∈ HAtoms p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
42 41 adantr ⊢ c ∈ C ℋ ∧ A ⊆ c → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A ↔ ∀ p ∈ HAtoms p ⊆ c ∩ B ∨ ℋ A → p ⊆ c ∩ B ∨ ℋ A
43 34 42 sylibrd ⊢ c ∈ C ℋ ∧ A ⊆ c → ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
44 43 ex ⊢ c ∈ C ℋ → A ⊆ c → ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
45 44 com3r ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → c ∈ C ℋ → A ⊆ c → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
46 45 ralrimiv ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → ∀ c ∈ C ℋ A ⊆ c → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
47 dmdbr2 ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → B 𝑀 ℋ * A ↔ ∀ c ∈ C ℋ A ⊆ c → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
48 2 1 47 mp2an ⊢ B 𝑀 ℋ * A ↔ ∀ c ∈ C ℋ A ⊆ c → c ∩ B ∨ ℋ A ⊆ c ∩ B ∨ ℋ A
49 46 48 sylibr ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → B 𝑀 ℋ * A