Metamath Proof Explorer

Theorem csmdsymi

Description: Cross-symmetry implies M-symmetry. Theorem 1.9.1 of MaedaMaeda p. 3. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses csmdsym.1 ⊢ 𝐴 ∈ Cℋ
csmdsym.2 ⊢ 𝐵 ∈ Cℋ
Assertion csmdsymi ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → 𝐵 𝑀ℋ 𝐴 )

Proof

Step Hyp Ref Expression
1 csmdsym.1 ⊢ 𝐴 ∈ Cℋ
2 csmdsym.2 ⊢ 𝐵 ∈ Cℋ
3 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
4 3 sseq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐵 ∩ 𝐴 ) ⊆ 𝑥 )
5 4 biimpri ⊢ ( ( 𝐵 ∩ 𝐴 ) ⊆ 𝑥 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 )
6 chjcom ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝑥 ) )
7 2 6 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝑥 ) )
8 7 ineq1d ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( 𝐵 ∨ℋ 𝑥 ) ∩ 𝐴 ) )
9 incom ⊢ ( ( 𝐵 ∨ℋ 𝑥 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝑥 ) )
10 8 9 eqtrdi ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝑥 ) ) )
11 10 ad2antlr ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝑥 ) ) )
12 2 a1i ⊢ ( 𝑥 ∈ Cℋ → 𝐵 ∈ Cℋ )
13 id ⊢ ( 𝑥 ∈ Cℋ → 𝑥 ∈ Cℋ )
14 1 a1i ⊢ ( 𝑥 ∈ Cℋ → 𝐴 ∈ Cℋ )
15 12 13 14 3jca ⊢ ( 𝑥 ∈ Cℋ → ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) )
16 15 ad2antlr ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) )
17 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
18 ssid ⊢ 𝐵 ⊆ 𝐵
19 17 18 pm3.2i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 )
20 sseq2 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐴 ∩ 𝐵 ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ) )
21 sseq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 ⊆ 𝐴 ↔ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ 𝐴 ) )
22 20 21 anbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ 𝐴 ) ) )
23 22 3anbi2d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) ↔ ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) ) )
24 breq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 𝑀ℋ 𝐵 ↔ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) 𝑀ℋ 𝐵 ) )
25 23 24 imbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → 𝑥 𝑀ℋ 𝐵 ) ↔ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) 𝑀ℋ 𝐵 ) ) )
26 h0elch ⊢ 0ℋ ∈ Cℋ
27 26 elimel ⊢ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∈ Cℋ
28 1 2 27 2 mdslmd4i ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) 𝑀ℋ 𝐵 )
29 25 28 dedth ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → 𝑥 𝑀ℋ 𝐵 ) )
30 29 com12 ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → ( 𝑥 ∈ Cℋ → 𝑥 𝑀ℋ 𝐵 ) )
31 19 30 mp3an3 ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( 𝑥 ∈ Cℋ → 𝑥 𝑀ℋ 𝐵 ) )
32 31 imp ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) → 𝑥 𝑀ℋ 𝐵 )
33 32 an32s ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 𝑀ℋ 𝐵 )
34 33 adantlll ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 𝑀ℋ 𝐵 )
35 breq1 ⊢ ( 𝑐 = 𝑥 → ( 𝑐 𝑀ℋ 𝐵 ↔ 𝑥 𝑀ℋ 𝐵 ) )
36 breq2 ⊢ ( 𝑐 = 𝑥 → ( 𝐵 𝑀ℋ* 𝑐 ↔ 𝐵 𝑀ℋ* 𝑥 ) )
37 35 36 imbi12d ⊢ ( 𝑐 = 𝑥 → ( ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ↔ ( 𝑥 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑥 ) ) )
38 37 rspccva ⊢ ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑥 ) )
39 38 adantlr ⊢ ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑥 ) )
40 39 adantr ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( 𝑥 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑥 ) )
41 34 40 mpd ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝐵 𝑀ℋ* 𝑥 )
42 simprr ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → 𝑥 ⊆ 𝐴 )
43 dmdi ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝑥 ) ) )
44 16 41 42 43 syl12anc ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝑥 ) ) )
45 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
46 chjcom ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
47 45 46 mpan ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
48 3 oveq2i ⊢ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) )
49 47 48 eqtrdi ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) )
50 49 ad2antlr ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) )
51 11 44 50 3eqtr2d ⊢ ( ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) )
52 51 ex ⊢ ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) )
53 5 52 sylani ⊢ ( ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝐵 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) )
54 53 ralrimiva ⊢ ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → ∀ 𝑥 ∈ Cℋ ( ( ( 𝐵 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) )
55 2 1 mdsl2bi ⊢ ( 𝐵 𝑀ℋ 𝐴 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐵 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) )
56 54 55 sylibr ⊢ ( ( ∀ 𝑐 ∈ Cℋ ( 𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → 𝐵 𝑀ℋ 𝐴 )