Theorem com2or 483

Description: Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)

Hypotheses

Ref	Expression
fh.1	a C b
fh.2	a C c

Assertion

Ref	Expression
com2or	a C (b ∪ c)

Proof of Theorem com2or

Step	Hyp	Ref	Expression
1		fh.1	. . . . . . . . 9 a C b
2	1	comcom 453	. . . . . . . 8 b C a
3	2	df-c2 133	. . . . . . 7 b = ((b ∩ a) ∪ (b ∩ a⊥ ))
4		ancom 74	. . . . . . . 8 (b ∩ a) = (a ∩ b)
5		ancom 74	. . . . . . . 8 (b ∩ a⊥ ) = (a⊥ ∩ b)
6	4, 5	2or 72	. . . . . . 7 ((b ∩ a) ∪ (b ∩ a⊥ )) = ((a ∩ b) ∪ (a⊥ ∩ b))
7	3, 6	ax-r2 36	. . . . . 6 b = ((a ∩ b) ∪ (a⊥ ∩ b))
8		fh.2	. . . . . . . . 9 a C c
9	8	comcom 453	. . . . . . . 8 c C a
10	9	df-c2 133	. . . . . . 7 c = ((c ∩ a) ∪ (c ∩ a⊥ ))
11		ancom 74	. . . . . . . 8 (c ∩ a) = (a ∩ c)
12		ancom 74	. . . . . . . 8 (c ∩ a⊥ ) = (a⊥ ∩ c)
13	11, 12	2or 72	. . . . . . 7 ((c ∩ a) ∪ (c ∩ a⊥ )) = ((a ∩ c) ∪ (a⊥ ∩ c))
14	10, 13	ax-r2 36	. . . . . 6 c = ((a ∩ c) ∪ (a⊥ ∩ c))
15	7, 14	2or 72	. . . . 5 (b ∪ c) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ c) ∪ (a⊥ ∩ c)))
16		or4 84	. . . . 5 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ c) ∪ (a⊥ ∩ c))) = (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))
17	15, 16	ax-r2 36	. . . 4 (b ∪ c) = (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))
18		ancom 74	. . . . . . 7 ((b ∪ c) ∩ a) = (a ∩ (b ∪ c))
19	1, 8	fh1 469	. . . . . . 7 (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
20	18, 19	ax-r2 36	. . . . . 6 ((b ∪ c) ∩ a) = ((a ∩ b) ∪ (a ∩ c))
21		ancom 74	. . . . . . 7 ((b ∪ c) ∩ a⊥ ) = (a⊥ ∩ (b ∪ c))
22	1	comcom3 454	. . . . . . . 8 a⊥ C b
23	8	comcom3 454	. . . . . . . 8 a⊥ C c
24	22, 23	fh1 469	. . . . . . 7 (a⊥ ∩ (b ∪ c)) = ((a⊥ ∩ b) ∪ (a⊥ ∩ c))
25	21, 24	ax-r2 36	. . . . . 6 ((b ∪ c) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ c))
26	20, 25	2or 72	. . . . 5 (((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ )) = (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))
27	26	ax-r1 35	. . . 4 (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c))) = (((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ ))
28	17, 27	ax-r2 36	. . 3 (b ∪ c) = (((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ ))
29	28	df-c1 132	. 2 (b ∪ c) C a
30	29	comcom 453	1 a C (b ∪ c)

Syntax hints:   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  com2an  484  combi  485  gsth  489  gsth2  490  gt1  492  dfi3b  499  oi3ai3  503  comi31  508  com2i3  509  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem3  562  ud3lem1a  566  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem3a  591  ud5lem3  594  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u3lemanb  617  u4lemanb  618  u5lemanb  619  u4lemona  628  u3lemob  632  u3lemonb  637  u1lemc1  680  u2lemc1  681  u4lemc1  683  u5lemc1  684  u5lemc1b  685  u1lemc2  686  u2lemc2  687  u4lemc2  689  u5lemc2  690  u4lemle2  718  u5lemle2  719  u5lembi  725  u4lem1  737  u4lem4  759  u4lem5  764  u4lem6  768  u24lem  770  u1lem8  776  u1lem11  780  u3lem13a  789  u3lem13b  790  u3lem15  795  test  802  test2  803  3vded21  817  mlalem  832  mlaconj4  844  neg3antlem2  865  mhlem  876  e2ast2  894  e2astlem1  895  govar  896