Theorem mdbr4

Description: Binary relation expressing the 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	mdbr4	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdbr2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
2		chincl	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∩ 𝐵 ) ∈ Cℋ )
3		inss2	⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵
4		sseq1	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ⊆ 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) )
5		oveq1	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ∨ℋ 𝐴 ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
6	5	ineq1d	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) )
7		oveq1	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
8	6 7	sseq12d	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
9	4 8	imbi12d	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
10	9	rspcv	⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
11	3 10	mpii	⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
12	2 11	syl	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
13	12	ex	⊢ ( 𝑥 ∈ Cℋ → ( 𝐵 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
14	13	com3l	⊢ ( 𝐵 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 ∈ Cℋ → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
15	14	ralrimdv	⊢ ( 𝐵 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
16		dfss	⊢ ( 𝑥 ⊆ 𝐵 ↔ 𝑥 = ( 𝑥 ∩ 𝐵 ) )
17	16	biimpi	⊢ ( 𝑥 ⊆ 𝐵 → 𝑥 = ( 𝑥 ∩ 𝐵 ) )
18	17	oveq1d	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∨ℋ 𝐴 ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
19	18	ineq1d	⊢ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) )
20	17	oveq1d	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
21	19 20	sseq12d	⊢ ( 𝑥 ⊆ 𝐵 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
22	21	biimprcd	⊢ ( ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
23	22	ralimi	⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
24		sseq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵 ) )
25		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∨ℋ 𝐴 ) = ( 𝑦 ∨ℋ 𝐴 ) )
26	25	ineq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
27		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
28	26 27	sseq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
29	24 28	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
30	29	cbvralvw	⊢ ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
31	23 30	sylib	⊢ ( ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
32	15 31	impbid1	⊢ ( 𝐵 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
33	32	adantl	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐵 → ( ( 𝑦 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑦 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
34	1 33	bitrd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )