Theorem 3vded22 800

Description: A 3-variable theorem. Experiment with weak deduction theorem.

Hypotheses

Ref	Expression
3vded22.1	c ≤ ( C (a, b) ∪ C (c, b))
3vded22.2	c ≤ a
3vded22.3	c ≤ (a →0 b)

Assertion

Ref	Expression
3vded22	c ≤ b

Proof of Theorem 3vded22

Step	Hyp	Ref	Expression
1		3vded22.1	. . . 4 c ≤ ( C (a, b) ∪ C (c, b))
2		df-cmtr 126	. . . . . . 7 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
3		or4 77	. . . . . . 7 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )))
4	2, 3	ax-r2 35	. . . . . 6 C (a, b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )))
5		lear 153	. . . . . . . 8 (a ∩ b) ≤ b
6		lear 153	. . . . . . . 8 (a⊥ ∩ b) ≤ b
7	5, 6	lel2or 162	. . . . . . 7 ((a ∩ b) ∪ (a⊥ ∩ b)) ≤ b
8		3vded22.2	. . . . . . . . . 10 c ≤ a
9	8	lecon 146	. . . . . . . . 9 a⊥ ≤ c⊥
10	9	leran 145	. . . . . . . 8 (a⊥ ∩ b⊥ ) ≤ (c⊥ ∩ b⊥ )
11	10	lelor 158	. . . . . . 7 ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )) ≤ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))
12	7, 11	le2or 160	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ))) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
13	4, 12	bltr 130	. . . . 5 C (a, b) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
14		df-cmtr 126	. . . . . . 7 C (c, b) = (((c ∩ b) ∪ (c ∩ b⊥ )) ∪ ((c⊥ ∩ b) ∪ (c⊥ ∩ b⊥ )))
15		or4 77	. . . . . . 7 (((c ∩ b) ∪ (c ∩ b⊥ )) ∪ ((c⊥ ∩ b) ∪ (c⊥ ∩ b⊥ ))) = (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
16	14, 15	ax-r2 35	. . . . . 6 C (c, b) = (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
17		lear 153	. . . . . . . 8 (c ∩ b) ≤ b
18		lear 153	. . . . . . . 8 (c⊥ ∩ b) ≤ b
19	17, 18	lel2or 162	. . . . . . 7 ((c ∩ b) ∪ (c⊥ ∩ b)) ≤ b
20	8	leran 145	. . . . . . . 8 (c ∩ b⊥ ) ≤ (a ∩ b⊥ )
21	20	leror 144	. . . . . . 7 ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )) ≤ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))
22	19, 21	le2or 160	. . . . . 6 (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
23	16, 22	bltr 130	. . . . 5 C (c, b) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
24	13, 23	le2or 160	. . . 4 ( C (a, b) ∪ C (c, b)) ≤ ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
25	1, 24	letr 129	. . 3 c ≤ ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
26		df-i0 42	. . . . 5 ((a →0 b) →0 (c →2 b)) = ((a →0 b)⊥ ∪ (c →2 b))
27		or12 73	. . . . . 6 ((a ∩ b⊥ ) ∪ (b ∪ (c⊥ ∩ b⊥ ))) = (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
28		df-i0 42	. . . . . . . . 9 (a →0 b) = (a⊥ ∪ b)
29	28	ax-r4 36	. . . . . . . 8 (a →0 b)⊥ = (a⊥ ∪ b)⊥
30		anor1 80	. . . . . . . . 9 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
31	30	ax-r1 34	. . . . . . . 8 (a⊥ ∪ b)⊥ = (a ∩ b⊥ )
32	29, 31	ax-r2 35	. . . . . . 7 (a →0 b)⊥ = (a ∩ b⊥ )
33		df-i2 44	. . . . . . 7 (c →2 b) = (b ∪ (c⊥ ∩ b⊥ ))
34	32, 33	2or 67	. . . . . 6 ((a →0 b)⊥ ∪ (c →2 b)) = ((a ∩ b⊥ ) ∪ (b ∪ (c⊥ ∩ b⊥ )))
35		oridm 102	. . . . . 6 ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))) = (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
36	27, 34, 35	3tr1 60	. . . . 5 ((a →0 b)⊥ ∪ (c →2 b)) = ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
37	26, 36	ax-r2 35	. . . 4 ((a →0 b) →0 (c →2 b)) = ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
38	37	ax-r1 34	. . 3 ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))) = ((a →0 b) →0 (c →2 b))
39	25, 38	lbtr 131	. 2 c ≤ ((a →0 b) →0 (c →2 b))
40		3vded22.3	. 2 c ≤ (a →0 b)
41	39, 40	3vded21 799	1 c ≤ b

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₀ wi0 12   →₂ wi2 14   C wcmtr 28

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i0 42  df-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125  df-cmtr 126

metamath.org