dmdbr4

Description: Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	dmdbr4	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 𝑀_ℋ^* 𝐵 ↔ ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmdbr2	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 𝑀_ℋ^* 𝐵 ↔ ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
2		chub2	⊢ ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) → 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) )
3	2	ancoms	⊢ ( ( 𝑥 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) )
4		chjcl	⊢ ( ( 𝑥 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝑥 ∨_ℋ 𝐵 ) ∈ C_ℋ )
5		sseq2	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) ) )
6		ineq1	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) )
7		ineq1	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( 𝑦 ∩ 𝐴 ) = ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) )
8	7	oveq1d	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) = ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) )
9	6 8	sseq12d	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ↔ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
10	5 9	imbi12d	⊢ ( 𝑦 = ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ↔ ( 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
11	10	rspcv	⊢ ( ( 𝑥 ∨_ℋ 𝐵 ) ∈ C_ℋ → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ( 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
12	4 11	syl	⊢ ( ( 𝑥 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ( 𝐵 ⊆ ( 𝑥 ∨_ℋ 𝐵 ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
13	3 12	mpid	⊢ ( ( 𝑥 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
14	13	ex	⊢ ( 𝑥 ∈ C_ℋ → ( 𝐵 ∈ C_ℋ → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
15	14	com3l	⊢ ( 𝐵 ∈ C_ℋ → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ( 𝑥 ∈ C_ℋ → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
16	15	ralrimdv	⊢ ( 𝐵 ∈ C_ℋ → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) → ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
17		chlejb2	⊢ ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) → ( 𝐵 ⊆ 𝑥 ↔ ( 𝑥 ∨_ℋ 𝐵 ) = 𝑥 ) )
18	17	biimpa	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( 𝑥 ∨_ℋ 𝐵 ) = 𝑥 )
19	18	ineq1d	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) )
20	18	ineq1d	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) )
21	20	oveq1d	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) = ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) )
22	19 21	sseq12d	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ↔ ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
23	22	biimpd	⊢ ( ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) ∧ 𝐵 ⊆ 𝑥 ) → ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
24	23	ex	⊢ ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
25	24	com23	⊢ ( ( 𝐵 ∈ C_ℋ ∧ 𝑥 ∈ C_ℋ ) → ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) → ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
26	25	ralimdva	⊢ ( 𝐵 ∈ C_ℋ → ( ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) → ∀ 𝑥 ∈ C_ℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
27		sseq2	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦 ) )
28		ineq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) = ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) )
29		ineq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∩ 𝐴 ) = ( 𝑦 ∩ 𝐴 ) )
30	29	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) = ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) )
31	28 30	sseq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ↔ ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
32	27 31	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ↔ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
33	32	cbvralvw	⊢ ( ∀ 𝑥 ∈ C_ℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ↔ ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
34	26 33	syl6ib	⊢ ( 𝐵 ∈ C_ℋ → ( ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) → ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ) )
35	16 34	impbid	⊢ ( 𝐵 ∈ C_ℋ → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ↔ ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
36	35	adantl	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ∀ 𝑦 ∈ C_ℋ ( 𝐵 ⊆ 𝑦 → ( 𝑦 ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( 𝑦 ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) ↔ ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )
37	1 36	bitrd	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( 𝐴 𝑀_ℋ^* 𝐵 ↔ ∀ 𝑥 ∈ C_ℋ ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )

Metamath Proof Explorer

Theorem dmdbr4

Proof