Theorem dmdbr4 10233

Description: Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference.

Assertion

Ref	Expression
dmdbr4	|- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))

Distinct variable groups:   x,A   x,B

Proof of Theorem dmdbr4

Step	Hyp	Ref	Expression
1		dmdbr2 10230	. 2 |- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B))))
2		chub2t 9431	. . . . . . . . 9 |- ((B e. CH /\ x e. CH) -> B (_ (x vH B))
3	2	ancoms 436	. . . . . . . 8 |- ((x e. CH /\ B e. CH) -> B (_ (x vH B))
4		chjclt 9329	. . . . . . . . 9 |- ((x e. CH /\ B e. CH) -> (x vH B) e. CH)
5		sseq2 2083	. . . . . . . . . . 11 |- (y = (x vH B) -> (B (_ y <-> B (_ (x vH B)))
6		ineq1 2210	. . . . . . . . . . . 12 |- (y = (x vH B) -> (y i^i (A vH B)) = ((x vH B) i^i (A vH B)))
7		ineq1 2210	. . . . . . . . . . . . 13 |- (y = (x vH B) -> (y i^i A) = ((x vH B) i^i A))
8	7	opreq1d 3975	. . . . . . . . . . . 12 |- (y = (x vH B) -> ((y i^i A) vH B) = (((x vH B) i^i A) vH B))
9	6, 8	sseq12d 2090	. . . . . . . . . . 11 |- (y = (x vH B) -> ((y i^i (A vH B)) (_ ((y i^i A) vH B) <-> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
10	5, 9	imbi12d 626	. . . . . . . . . 10 |- (y = (x vH B) -> ((B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) <-> (B (_ (x vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
11	10	rcla4v 1873	. . . . . . . . 9 |- ((x vH B) e. CH -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> (B (_ (x vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
12	4, 11	syl 10	. . . . . . . 8 |- ((x e. CH /\ B e. CH) -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> (B (_ (x vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
13	3, 12	mpid 47	. . . . . . 7 |- ((x e. CH /\ B e. CH) -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
14	13	ex 373	. . . . . 6 |- (x e. CH -> (B e. CH -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
15	14	com3l 34	. . . . 5 |- (B e. CH -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> (x e. CH -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
16	15	r19.21adv 1718	. . . 4 |- (B e. CH -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) -> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
17		chlejb2t 9436	. . . . . . . . . . . 12 |- ((B e. CH /\ x e. CH) -> (B (_ x <-> (x vH B) = x))
18	17	biimpa 416	. . . . . . . . . . 11 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> (x vH B) = x)
19	18	ineq1d 2216	. . . . . . . . . 10 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> ((x vH B) i^i (A vH B)) = (x i^i (A vH B)))
20	18	ineq1d 2216	. . . . . . . . . . 11 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> ((x vH B) i^i A) = (x i^i A))
21	20	opreq1d 3975	. . . . . . . . . 10 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> (((x vH B) i^i A) vH B) = ((x i^i A) vH B))
22	19, 21	sseq12d 2090	. . . . . . . . 9 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) <-> (x i^i (A vH B)) (_ ((x i^i A) vH B)))
23	22	biimpd 153	. . . . . . . 8 |- (((B e. CH /\ x e. CH) /\ B (_ x) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (x i^i (A vH B)) (_ ((x i^i A) vH B)))
24	23	ex 373	. . . . . . 7 |- ((B e. CH /\ x e. CH) -> (B (_ x -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (x i^i (A vH B)) (_ ((x i^i A) vH B))))
25	24	com23 32	. . . . . 6 |- ((B e. CH /\ x e. CH) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (B (_ x -> (x i^i (A vH B)) (_ ((x i^i A) vH B))))
26	25	r19.20dva 1709	. . . . 5 |- (B e. CH -> (A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> A.x e. CH (B (_ x -> (x i^i (A vH B)) (_ ((x i^i A) vH B))))
27		sseq2 2083	. . . . . . 7 |- (x = y -> (B (_ x <-> B (_ y))
28		ineq1 2210	. . . . . . . 8 |- (x = y -> (x i^i (A vH B)) = (y i^i (A vH B)))
29		ineq1 2210	. . . . . . . . 9 |- (x = y -> (x i^i A) = (y i^i A))
30	29	opreq1d 3975	. . . . . . . 8 |- (x = y -> ((x i^i A) vH B) = ((y i^i A) vH B))
31	28, 30	sseq12d 2090	. . . . . . 7 |- (x = y -> ((x i^i (A vH B)) (_ ((x i^i A) vH B) <-> (y i^i (A vH B)) (_ ((y i^i A) vH B)))
32	27, 31	imbi12d 626	. . . . . 6 |- (x = y -> ((B (_ x -> (x i^i (A vH B)) (_ ((x i^i A) vH B)) <-> (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B))))
33	32	cbvralv 1800	. . . . 5 |- (A.x e. CH (B (_ x -> (x i^i (A vH B)) (_ ((x i^i A) vH B)) <-> A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)))
34	26, 33	syl6ib 212	. . . 4 |- (B e. CH -> (A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B))))
35	16, 34	impbid 516	. . 3 |- (B e. CH -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) <-> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
36	35	adantl 388	. 2 |- ((A e. CH /\ B e. CH) -> (A.y e. CH (B (_ y -> (y i^i (A vH B)) (_ ((y i^i A) vH B)) <-> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
37	1, 36	bitrd 528	1 |- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  A.wral 1645   i^i cin 2046   (_ wss 2047   class class class wbr 2619  (class class class)co 3963  CHcch 8798   vH chj 8802   MH* cdmd 8836

This theorem is referenced by:  dmdi4 10234  dmdbr5 10235  sumdmd 10347  dmdbr4at 10348

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-reg 4593  ax-inf2 4625  ax-ac 4744  ax-hilex 8869  ax-hfvadd 8870  ax-hvcom 8871  ax-hvass 8872  ax-hv0cl 8873  ax-hvaddid 8874  ax-hfvmul 8875  ax-hvmulid 8876  ax-hvmulass 8877  ax-hvdistr1 8878  ax-hvdistr2 8879  ax-hvmul0 8880  ax-hfi 8946  ax-his1 8949  ax-his2 8950  ax-his3 8951  ax-his4 8952  ax-hcompl 9071

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-nel 1588  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-pss 2055  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-iun 2568  df-iin 2569  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we