Theorem gsth2 490

Description: Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Thm. 4.2. (Contributed by NM, 20-Sep-1998.)

Hypotheses

Ref	Expression
gsth2.1	b C c
gsth2.2	a C (b ∩ c)

Assertion

Ref	Expression
gsth2	(a ∩ b) C c

Proof of Theorem gsth2

Step	Hyp	Ref	Expression
1		gsth2.1	. . . . 5 b C c
2	1	comcom 453	. . . 4 c C b
3		ancom 74	. . . . . . . . 9 (b ∩ (b⊥ ∪ a⊥ )) = ((b⊥ ∪ a⊥ ) ∩ b)
4		ax-a2 31	. . . . . . . . . 10 (b⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
5	4	ran 78	. . . . . . . . 9 ((b⊥ ∪ a⊥ ) ∩ b) = ((a⊥ ∪ b⊥ ) ∩ b)
6	3, 5	ax-r2 36	. . . . . . . 8 (b ∩ (b⊥ ∪ a⊥ )) = ((a⊥ ∪ b⊥ ) ∩ b)
7		comor2 462	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C b⊥
8	7	comcom7 460	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C b
9		gsth2.2	. . . . . . . . . . . . 13 a C (b ∩ c)
10	9	comcom 453	. . . . . . . . . . . 12 (b ∩ c) C a
11	10	comcom2 183	. . . . . . . . . . 11 (b ∩ c) C a⊥
12		coman1 185	. . . . . . . . . . . 12 (b ∩ c) C b
13	12	comcom2 183	. . . . . . . . . . 11 (b ∩ c) C b⊥
14	11, 13	com2or 483	. . . . . . . . . 10 (b ∩ c) C (a⊥ ∪ b⊥ )
15	14	comcom 453	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C (b ∩ c)
16	8, 1, 15	gsth 489	. . . . . . . 8 ((a⊥ ∪ b⊥ ) ∩ b) C c
17	6, 16	bctr 181	. . . . . . 7 (b ∩ (b⊥ ∪ a⊥ )) C c
18	17	comcom 453	. . . . . 6 c C (b ∩ (b⊥ ∪ a⊥ ))
19		df-a 40	. . . . . . 7 (b ∩ (b⊥ ∪ a⊥ )) = (b⊥ ∪ (b⊥ ∪ a⊥ )⊥ )⊥
20		df-a 40	. . . . . . . . . 10 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
21	20	lor 70	. . . . . . . . 9 (b⊥ ∪ (b ∩ a)) = (b⊥ ∪ (b⊥ ∪ a⊥ )⊥ )
22	21	ax-r4 37	. . . . . . . 8 (b⊥ ∪ (b ∩ a))⊥ = (b⊥ ∪ (b⊥ ∪ a⊥ )⊥ )⊥
23	22	ax-r1 35	. . . . . . 7 (b⊥ ∪ (b⊥ ∪ a⊥ )⊥ )⊥ = (b⊥ ∪ (b ∩ a))⊥
24	19, 23	ax-r2 36	. . . . . 6 (b ∩ (b⊥ ∪ a⊥ )) = (b⊥ ∪ (b ∩ a))⊥
25	18, 24	cbtr 182	. . . . 5 c C (b⊥ ∪ (b ∩ a))⊥
26	25	comcom7 460	. . . 4 c C (b⊥ ∪ (b ∩ a))
27	2, 26	com2an 484	. . 3 c C (b ∩ (b⊥ ∪ (b ∩ a)))
28		omla 447	. . . 4 (b ∩ (b⊥ ∪ (b ∩ a))) = (b ∩ a)
29		ancom 74	. . . 4 (b ∩ a) = (a ∩ b)
30	28, 29	ax-r2 36	. . 3 (b ∩ (b⊥ ∪ (b ∩ a))) = (a ∩ b)
31	27, 30	cbtr 182	. 2 c C (a ∩ b)
32	31	comcom 453	1 (a ∩ b) C c

This proof depends on syntax axioms:   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on 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 proof 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 used by:  gstho  491  oacom  1011  oacom3  1013