Metamath Proof Explorer


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 A C B C A 𝑀 B x C x B A B x B A B

Proof

Step Hyp Ref Expression
1 mdbr2 A C B C A 𝑀 B y C y B y A B y A B
2 chincl x C B C x B C
3 inss2 x B B
4 sseq1 y = x B y B x B B
5 oveq1 y = x B y A = x B A
6 5 ineq1d y = x B y A B = x B A B
7 oveq1 y = x B y A B = x B A B
8 6 7 sseq12d y = x B y A B y A B x B A B x B A B
9 4 8 imbi12d y = x B y B y A B y A B x B B x B A B x B A B
10 9 rspcv x B C y C y B y A B y A B x B B x B A B x B A B
11 3 10 mpii x B C y C y B y A B y A B x B A B x B A B
12 2 11 syl x C B C y C y B y A B y A B x B A B x B A B
13 12 ex x C B C y C y B y A B y A B x B A B x B A B
14 13 com3l B C y C y B y A B y A B x C x B A B x B A B
15 14 ralrimdv B C y C y B y A B y A B x C x B A B x B A B
16 dfss x B x = x B
17 16 biimpi x B x = x B
18 17 oveq1d x B x A = x B A
19 18 ineq1d x B x A B = x B A B
20 17 oveq1d x B x A B = x B A B
21 19 20 sseq12d x B x A B x A B x B A B x B A B
22 21 biimprcd x B A B x B A B x B x A B x A B
23 22 ralimi x C x B A B x B A B x C x B x A B x A B
24 sseq1 x = y x B y B
25 oveq1 x = y x A = y A
26 25 ineq1d x = y x A B = y A B
27 oveq1 x = y x A B = y A B
28 26 27 sseq12d x = y x A B x A B y A B y A B
29 24 28 imbi12d x = y x B x A B x A B y B y A B y A B
30 29 cbvralvw x C x B x A B x A B y C y B y A B y A B
31 23 30 sylib x C x B A B x B A B y C y B y A B y A B
32 15 31 impbid1 B C y C y B y A B y A B x C x B A B x B A B
33 32 adantl A C B C y C y B y A B y A B x C x B A B x B A B
34 1 33 bitrd A C B C A 𝑀 B x C x B A B x B A B