Metamath Proof Explorer

Theorem mdsymlem8

Description: Lemma for mdsymi . Lemma 4(ii) of Maeda p. 168. (Contributed by NM, 3-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢A∈Cℋ
mdsymlem1.2 ⊢B∈Cℋ
mdsymlem1.3 ⊢C=A∨ℋp
Assertion mdsymlem8 ⊢A≠0ℋ∧B≠0ℋ→B𝑀ℋ*A↔A𝑀ℋ*B

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 atelch ⊢q∈HAtoms→q∈Cℋ
7 atelch ⊢r∈HAtoms→r∈Cℋ
8 chjcom ⊢q∈Cℋ∧r∈Cℋ→q∨ℋr=r∨ℋq
9 6 7 8 syl2an ⊢q∈HAtoms∧r∈HAtoms→q∨ℋr=r∨ℋq
10 9 sseq2d ⊢q∈HAtoms∧r∈HAtoms→p⊆q∨ℋr↔p⊆r∨ℋq
11 ancom ⊢q⊆A∧r⊆B↔r⊆B∧q⊆A
12 11 a1i ⊢q∈HAtoms∧r∈HAtoms→q⊆A∧r⊆B↔r⊆B∧q⊆A
13 10 12 anbi12d ⊢q∈HAtoms∧r∈HAtoms→p⊆q∨ℋr∧q⊆A∧r⊆B↔p⊆r∨ℋq∧r⊆B∧q⊆A
14 13 2rexbiia ⊢∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B↔∃q∈HAtoms∃r∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
15 rexcom ⊢∃q∈HAtoms∃r∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A↔∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
16 14 15 bitri ⊢∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B↔∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
17 5 16 imbi12i ⊢p⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B↔p⊆B∨ℋA→∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
18 17 ralbii ⊢∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B↔∀p∈HAtomsp⊆B∨ℋA→∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
19 18 a1i ⊢A≠0ℋ∧B≠0ℋ→∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B↔∀p∈HAtomsp⊆B∨ℋA→∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
20 1 2 3 mdsymlem7 ⊢A≠0ℋ∧B≠0ℋ→B𝑀ℋ*A↔∀p∈HAtomsp⊆A∨ℋB→∃q∈HAtoms∃r∈HAtomsp⊆q∨ℋr∧q⊆A∧r⊆B
21 eqid ⊢B∨ℋp=B∨ℋp
22 2 1 21 mdsymlem7 ⊢B≠0ℋ∧A≠0ℋ→A𝑀ℋ*B↔∀p∈HAtomsp⊆B∨ℋA→∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
23 22 ancoms ⊢A≠0ℋ∧B≠0ℋ→A𝑀ℋ*B↔∀p∈HAtomsp⊆B∨ℋA→∃r∈HAtoms∃q∈HAtomsp⊆r∨ℋq∧r⊆B∧q⊆A
24 19 20 23 3bitr4d ⊢A≠0ℋ∧B≠0ℋ→B𝑀ℋ*A↔A𝑀ℋ*B