Theorem dmdbr5 10235

Description: Binary relation expressing the dual modular pair property.

Assertion

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

Distinct variable groups:   x,A   x,B

Proof of Theorem dmdbr5

Step	Hyp	Ref	Expression
1		dmdbr4 10233	. . 3 |- ((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)))
2		ssin 2232	. . . . . . . . 9 |- ((x (_ (x vH B) /\ x (_ (A vH B)) <-> x (_ ((x vH B) i^i (A vH B)))
3		sstr2 2071	. . . . . . . . 9 |- (x (_ ((x vH B) i^i (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
4	2, 3	sylbi 199	. . . . . . . 8 |- ((x (_ (x vH B) /\ x (_ (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
5		chub1t 9430	. . . . . . . . 9 |- ((x e. CH /\ B e. CH) -> x (_ (x vH B))
6	5	ancoms 436	. . . . . . . 8 |- ((B e. CH /\ x e. CH) -> x (_ (x vH B))
7	4, 6	sylan 448	. . . . . . 7 |- (((B e. CH /\ x e. CH) /\ x (_ (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
8	7	ex 373	. . . . . 6 |- ((B e. CH /\ x e. CH) -> (x (_ (A vH B) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B))))
9	8	com23 32	. . . . 5 |- ((B e. CH /\ x e. CH) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
10	9	r19.20dva 1709	. . . 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.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
11	10	adantl 388	. . 3 |- ((A e. CH /\ 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 (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
12	1, 11	sylbid 203	. 2 |- ((A e. CH /\ B e. CH) -> (A MH* B -> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
13		chjclt 9329	. . . . . . . . . . . 12 |- ((y e. CH /\ B e. CH) -> (y vH B) e. CH)
14	13	ancoms 436	. . . . . . . . . . 11 |- ((B e. CH /\ y e. CH) -> (y vH B) e. CH)
15	14	adantll 392	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (y vH B) e. CH)
16		chjclt 9329	. . . . . . . . . . 11 |- ((A e. CH /\ B e. CH) -> (A vH B) e. CH)
17	16	adantr 389	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (A vH B) e. CH)
18	15, 17	jca 288	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((y vH B) e. CH /\ (A vH B) e. CH))
19		chinclt 9422	. . . . . . . . 9 |- (((y vH B) e. CH /\ (A vH B) e. CH) -> ((y vH B) i^i (A vH B)) e. CH)
20		inss2 2231	. . . . . . . . . 10 |- ((y vH B) i^i (A vH B)) (_ (A vH B)
21		pm2.27 62	. . . . . . . . . 10 |- (((y vH B) i^i (A vH B)) e. CH -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))))
22	20, 21	mpii 45	. . . . . . . . 9 |- (((y vH B) i^i (A vH B)) e. CH -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B)))
23	18, 19, 22	3syl 20	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B)))
24		chub2t 9431	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ y e. CH) -> B (_ (y vH B))
25	24	adantll 392	. . . . . . . . . . . . . . 15 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ (y vH B))
26		chub2t 9431	. . . . . . . . . . . . . . . . 17 |- ((B e. CH /\ A e. CH) -> B (_ (A vH B))
27	26	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((A e. CH /\ B e. CH) -> B (_ (A vH B))
28	27	adantr 389	. . . . . . . . . . . . . . 15 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ (A vH B))
29	25, 28	jca 288	. . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (B (_ (y vH B) /\ B (_ (A vH B)))
30		ssin 2232	. . . . . . . . . . . . . 14 |- ((B (_ (y vH B) /\ B (_ (A vH B)) <-> B (_ ((y vH B) i^i (A vH B)))
31	29, 30	sylib 198	. . . . . . . . . . . . 13 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ ((y vH B) i^i (A vH B)))
32		chlejb2t 9436	. . . . . . . . . . . . . 14 |- ((B e. CH /\ ((y vH B) i^i (A vH B)) e. CH) -> (B (_ ((y vH B) i^i (A vH B)) <-> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B))))
33		simplr 413	. . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B e. CH)
34	19, 15, 17	sylanc 471	. . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((y vH B) i^i (A vH B)) e. CH)
35	32, 33, 34	sylanc 471	. . . . . . . . . . . . 13 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (B (_ ((y vH B) i^i (A vH B)) <-> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B))))
36	31, 35	mpbid 195	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B)))
37	36	ineq1d 2216	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((((y vH B) i^i (A vH B)) vH B) i^i A) = (((y vH B) i^i (A vH B)) i^i A))
38		chabs2t 9440	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ B e. CH) -> (A i^i (A vH B)) = A)
39		incom 2208	. . . . . . . . . . . . . . 15 |- ((A vH B) i^i A) = (A i^i (A vH B))
40	38, 39	syl5eq 1519	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> ((A vH B) i^i A) = A)
41	40	ineq2d 2217	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> ((y vH B) i^i ((A vH B) i^i A)) = ((y vH B) i^i A))
42		inass 2223	. . . . . . . . . . . . 13 |- (((y vH B) i^i (A vH B)) i^i A) = ((y vH B) i^i ((A vH B) i^i A))
43	41, 42	syl5eq 1519	. . . . . . . . . . . 12 |- ((A e. CH /\ B e. CH) -> (((y vH B) i^i (A vH B)) i^i A) = ((y vH B) i^i A))
44	43	adantr 389	. . . . . . . . . . 11 |- (((A e. CH /\ B e.