Theorem cvmdi 12727

Description: The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31.

Hypotheses

Ref	Expression
mdsl.1	|- A e. CH
mdsl.2	|- B e. CH

Assertion

Ref	Expression
cvmdi	|- ((A i^i B) <oℋ B -> A MH B)

Proof of Theorem cvmdi

Step	Hyp	Ref	Expression
1		anass 633	. . . . . 6 |- ((((A i^i B) C_ x /\ x C_ (A vH B)) /\ x C_ B) <-> ((A i^i B) C_ x /\ (x C_ (A vH B) /\ x C_ B)))
2		mdsl.2	. . . . . . . . . 10 |- B e. CH
3		mdsl.1	. . . . . . . . . 10 |- A e. CH
4	2, 3	chub2i 11860	. . . . . . . . 9 |- B C_ (A vH B)
5		sstr 2855	. . . . . . . . 9 |- ((x C_ B /\ B C_ (A vH B)) -> x C_ (A vH B))
6	4, 5	mpan2 679	. . . . . . . 8 |- (x C_ B -> x C_ (A vH B))
7	6	pm4.71ri 961	. . . . . . 7 |- (x C_ B <-> (x C_ (A vH B) /\ x C_ B))
8	7	anbi2i 708	. . . . . 6 |- (((A i^i B) C_ x /\ x C_ B) <-> ((A i^i B) C_ x /\ (x C_ (A vH B) /\ x C_ B)))
9	1, 8	bitr4i 283	. . . . 5 |- ((((A i^i B) C_ x /\ x C_ (A vH B)) /\ x C_ B) <-> ((A i^i B) C_ x /\ x C_ B))
10	3, 2	chincli 11850	. . . . . . . 8 |- (A i^i B) e. CH
11		cvnbtwn4 12692	. . . . . . . 8 |- (((A i^i B) e. CH /\ B e. CH /\ x e. CH) -> ((A i^i B) <oℋ B -> (((A i^i B) C_ x /\ x C_ B) -> (x = (A i^i B) \/ x = B))))
12	10, 2, 11	mp3an12 1456	. . . . . . 7 |- (x e. CH -> ((A i^i B) <oℋ B -> (((A i^i B) C_ x /\ x C_ B) -> (x = (A i^i B) \/ x = B))))
13	12	impcom 394	. . . . . 6 |- (((A i^i B) <oℋ B /\ x e. CH) -> (((A i^i B) C_ x /\ x C_ B) -> (x = (A i^i B) \/ x = B)))
14	10, 3	chjcomi 11858	. . . . . . . . . . 11 |- ((A i^i B) vH A) = (A vH (A i^i B))
15	3, 2	chabs1i 11908	. . . . . . . . . . 11 |- (A vH (A i^i B)) = A
16	14, 15	eqtri 2161	. . . . . . . . . 10 |- ((A i^i B) vH A) = A
17	16	ineq1i 3005	. . . . . . . . 9 |- (((A i^i B) vH A) i^i B) = (A i^i B)
18	10	chjidmi 11911	. . . . . . . . 9 |- ((A i^i B) vH (A i^i B)) = (A i^i B)
19	17, 18	eqtr4i 2164	. . . . . . . 8 |- (((A i^i B) vH A) i^i B) = ((A i^i B) vH (A i^i B))
20		opreq1 4986	. . . . . . . . 9 |- (x = (A i^i B) -> (x vH A) = ((A i^i B) vH A))
21	20	ineq1d 3008	. . . . . . . 8 |- (x = (A i^i B) -> ((x vH A) i^i B) = (((A i^i B) vH A) i^i B))
22		opreq1 4986	. . . . . . . 8 |- (x = (A i^i B) -> (x vH (A i^i B)) = ((A i^i B) vH (A i^i B)))
23	19, 21, 22	3eqtr4a 2202	. . . . . . 7 |- (x = (A i^i B) -> ((x vH A) i^i B) = (x vH (A i^i B)))
24		incom 3000	. . . . . . . . 9 |- ((B vH A) i^i B) = (B i^i (B vH A))
25	2, 3	chabs2i 11909	. . . . . . . . 9 |- (B i^i (B vH A)) = B
26	2, 3	chabs1i 11908	. . . . . . . . . 10 |- (B vH (B i^i A)) = B
27		incom 3000	. . . . . . . . . . 11 |- (B i^i A) = (A i^i B)
28	27	opreq2i 4990	. . . . . . . . . 10 |- (B vH (B i^i A)) = (B vH (A i^i B))
29	26, 28	eqtr3i 2163	. . . . . . . . 9 |- B = (B vH (A i^i B))
30	24, 25, 29	3eqtri 2165	. . . . . . . 8 |- ((B vH A) i^i B) = (B vH (A i^i B))
31		opreq1 4986	. . . . . . . . 9 |- (x = B -> (x vH A) = (B vH A))
32	31	ineq1d 3008	. . . . . . . 8 |- (x = B -> ((x vH A) i^i B) = ((B vH A) i^i B))
33		opreq1 4986	. . . . . . . 8 |- (x = B -> (x vH (A i^i B)) = (B vH (A i^i B)))
34	30, 32, 33	3eqtr4a 2202	. . . . . . 7 |- (x = B -> ((x vH A) i^i B) = (x vH (A i^i B)))
35	23, 34	jaoi 453	. . . . . 6 |- ((x = (A i^i B) \/ x = B) -> ((x vH A) i^i B) = (x vH (A i^i B)))
36	13, 35	syl6 42	. . . . 5 |- (((A i^i B) <oℋ B /\ x e. CH) -> (((A i^i B) C_ x /\ x C_ B) -> ((x vH A) i^i B) = (x vH (A i^i B))))
37	9, 36	syl5bi 249	. . . 4 |- (((A i^i B) <oℋ B /\ x e. CH) -> ((((A i^i B) C_ x /\ x C_ (A vH B)) /\ x C_ B) -> ((x vH A) i^i B) = (x vH (A i^i B))))
38	37	exp4b 580	. . 3 |- ((A i^i B) <oℋ B -> (x e. CH -> (((A i^i B) C_ x /\ x C_ (A vH B)) -> (x C_ B -> ((x vH A) i^i B) = (x vH (A i^i B))))))
39	38	r19.21aiv 2425	. 2 |- ((A i^i B) <oℋ B -> A.x e. CH (((A i^i B) C_ x /\ x C_ (A vH B)) -> (x C_ B -> ((x vH A) i^i B) = (x vH (A i^i B)))))
40	3, 2	mdsl1i 12724	. 2 |- (A.x e. CH (((A i^i B) C_ x /\ x C_ (A vH B)) -> (x C_ B -> ((x vH A) i^i B) = (x vH (A i^i B)))) <-> A MH B)
41	39, 40	sylib 242	1 |- ((A i^i B) <oℋ B -> A MH B)

Syntax hints:   -> wi 3   \/ wo 336   /\ wa 337   = wceq 1586   e. wcel 1588  A.wral 2355   i^i cin 2826   C_ wss 2827   class class class wbr 3507  (class class class)co 4981  CHcch 11268   vH chj 11272   <o_ℋ ccv 11304   MH cmd 11305

This theorem is referenced by:  cvmd 12739

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1590  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-reg 5928  ax-inf2 5964  ax-ac 6314  ax-hilex 11339  ax-hfvadd 11340  ax-hvcom 11341  ax-hvass 11342  ax-hv0cl 11343  ax-hvaddid 11344  ax-hfvmul 11345  ax-hvmulid 11346  ax-hvmulass 11347  ax-hvdistr1 11348  ax-hvdistr2 11349  ax-hvmul0 11350  ax-hfi 11416  ax-his1 11419  ax-his2 11420  ax-his3 11421  ax-his4 11422  ax-hcompl 11540

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-iin 3439  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-map 5544  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-r1 5986  df-rank 5987  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-3 7488  df-4 7489  df-n0 7649  df-z 7686  df-q 7782  df-fl 7809  df-ioo 7874  df-uz 7934  df-fz 7999  df-seq1 8094  df-shft 8129  df-seqz 8151  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388  df-clim 8631  df-sum 8636  df-top 9692  df-bases 9694  df-topgen 9695  df-cld 9800  df-ntr 9801  df-cls 9802  df-cn 9896  df-cnp 9897  df-haus 9925  df-met 9936  df-bl 9938  df-opn 9939  df-lm 10066  df-grpo 10182  df-gid 10183  df-ginv 10184  df-gdiv 10185  df-ablo 10277  df-vc 10366  df-nv 10412  df-va 10415  df-ba 10416  df-sm 10417  df-0v 10418  df-vs 10419  df-nm 10420  df-ims 10421  df-ip 10558  df-ph 10682  df-hnorm 11307  df-hvsub 11310  df-hlim 11311  df-hcau 11312  df-sh 11545  df-ch 11559  df-oc 11591  df-ch0 11592  df-shsum 11740  df-chj 11742  df-cv 12682  df-md 12683

Copyright terms: Public domain