Metamath Proof Explorer


Theorem mddmd2

Description: Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mddmd2 ( 𝐴C → ( ∀ 𝑥C 𝐴 𝑀 𝑥 ↔ ∀ 𝑥C 𝐴 𝑀* 𝑥 ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑥 = 𝑦 → ( 𝐴 𝑀 𝑥𝐴 𝑀 𝑦 ) )
2 1 cbvralvw ( ∀ 𝑥C 𝐴 𝑀 𝑥 ↔ ∀ 𝑦C 𝐴 𝑀 𝑦 )
3 mdbr ( ( 𝐴C𝑦C ) → ( 𝐴 𝑀 𝑦 ↔ ∀ 𝑥C ( 𝑥𝑦 → ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ( 𝐴𝑦 ) ) ) ) )
4 chjcom ( ( 𝐴C𝑥C ) → ( 𝐴 𝑥 ) = ( 𝑥 𝐴 ) )
5 4 ineq1d ( ( 𝐴C𝑥C ) → ( ( 𝐴 𝑥 ) ∩ 𝑦 ) = ( ( 𝑥 𝐴 ) ∩ 𝑦 ) )
6 incom ( ( 𝐴 𝑥 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) )
7 5 6 eqtr3di ( ( 𝐴C𝑥C ) → ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) )
8 7 adantlr ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) )
9 chincl ( ( 𝐴C𝑦C ) → ( 𝐴𝑦 ) ∈ C )
10 chjcom ( ( ( 𝐴𝑦 ) ∈ C𝑥C ) → ( ( 𝐴𝑦 ) ∨ 𝑥 ) = ( 𝑥 ( 𝐴𝑦 ) ) )
11 9 10 sylan ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( ( 𝐴𝑦 ) ∨ 𝑥 ) = ( 𝑥 ( 𝐴𝑦 ) ) )
12 incom ( 𝐴𝑦 ) = ( 𝑦𝐴 )
13 12 oveq1i ( ( 𝐴𝑦 ) ∨ 𝑥 ) = ( ( 𝑦𝐴 ) ∨ 𝑥 )
14 11 13 eqtr3di ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( 𝑥 ( 𝐴𝑦 ) ) = ( ( 𝑦𝐴 ) ∨ 𝑥 ) )
15 8 14 eqeq12d ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ( 𝐴𝑦 ) ) ↔ ( 𝑦 ∩ ( 𝐴 𝑥 ) ) = ( ( 𝑦𝐴 ) ∨ 𝑥 ) ) )
16 eqcom ( ( 𝑦 ∩ ( 𝐴 𝑥 ) ) = ( ( 𝑦𝐴 ) ∨ 𝑥 ) ↔ ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) )
17 15 16 bitrdi ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ( 𝐴𝑦 ) ) ↔ ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) )
18 17 imbi2d ( ( ( 𝐴C𝑦C ) ∧ 𝑥C ) → ( ( 𝑥𝑦 → ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ( 𝐴𝑦 ) ) ) ↔ ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
19 18 ralbidva ( ( 𝐴C𝑦C ) → ( ∀ 𝑥C ( 𝑥𝑦 → ( ( 𝑥 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ( 𝐴𝑦 ) ) ) ↔ ∀ 𝑥C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
20 3 19 bitrd ( ( 𝐴C𝑦C ) → ( 𝐴 𝑀 𝑦 ↔ ∀ 𝑥C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
21 20 ralbidva ( 𝐴C → ( ∀ 𝑦C 𝐴 𝑀 𝑦 ↔ ∀ 𝑦C𝑥C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
22 2 21 syl5bb ( 𝐴C → ( ∀ 𝑥C 𝐴 𝑀 𝑥 ↔ ∀ 𝑦C𝑥C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
23 ralcom ( ∀ 𝑦C𝑥C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ↔ ∀ 𝑥C𝑦C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) )
24 22 23 bitrdi ( 𝐴C → ( ∀ 𝑥C 𝐴 𝑀 𝑥 ↔ ∀ 𝑥C𝑦C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
25 dmdbr ( ( 𝐴C𝑥C ) → ( 𝐴 𝑀* 𝑥 ↔ ∀ 𝑦C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
26 25 ralbidva ( 𝐴C → ( ∀ 𝑥C 𝐴 𝑀* 𝑥 ↔ ∀ 𝑥C𝑦C ( 𝑥𝑦 → ( ( 𝑦𝐴 ) ∨ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 𝑥 ) ) ) ) )
27 24 26 bitr4d ( 𝐴C → ( ∀ 𝑥C 𝐴 𝑀 𝑥 ↔ ∀ 𝑥C 𝐴 𝑀* 𝑥 ) )