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∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆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∈HAtomsp⊆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∈HAtomsp⊆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∈HAtomsp⊆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∈HAtomsp⊆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∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→p⊆c∧p⊆A∨ℋB→p⊆c∩B∨ℋA
32 8 31 biimtrrid ⊢c∈Cℋ∧A⊆c∧p∈HAtoms∧p⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆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∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→p⊆c∩B∨ℋA→p⊆c∩B∨ℋA
34 33 ralimdva ⊢c∈Cℋ∧A⊆c→∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→∀p∈HAtomsp⊆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∈HAtomsp⊆c∩B∨ℋA→p⊆c∩B∨ℋA
41 37 39 40 syl2anc ⊢c∈Cℋ→c∩B∨ℋA⊆c∩B∨ℋA↔∀p∈HAtomsp⊆c∩B∨ℋA→p⊆c∩B∨ℋA
42 41 adantr ⊢c∈Cℋ∧A⊆c→c∩B∨ℋA⊆c∩B∨ℋA↔∀p∈HAtomsp⊆c∩B∨ℋA→p⊆c∩B∨ℋA
43 34 42 sylibrd ⊢c∈Cℋ∧A⊆c→∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→c∩B∨ℋA⊆c∩B∨ℋA
44 43 ex ⊢c∈Cℋ→A⊆c→∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→c∩B∨ℋA⊆c∩B∨ℋA
45 44 com3r ⊢∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→c∈Cℋ→A⊆c→c∩B∨ℋA⊆c∩B∨ℋA
46 45 ralrimiv ⊢∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆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∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B→B𝑀ℋ*A