Theorem 3vded22 818

Description: A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)

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 134	. . . . . . 7 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
3		or4 84	. . . . . . 7 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )))
4	2, 3	ax-r2 36	. . . . . 6 C (a, b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )))
5		lear 161	. . . . . . . 8 (a ∩ b) ≤ b
6		lear 161	. . . . . . . 8 (a⊥ ∩ b) ≤ b
7	5, 6	lel2or 170	. . . . . . 7 ((a ∩ b) ∪ (a⊥ ∩ b)) ≤ b
8		3vded22.2	. . . . . . . . . 10 c ≤ a
9	8	lecon 154	. . . . . . . . 9 a⊥ ≤ c⊥
10	9	leran 153	. . . . . . . 8 (a⊥ ∩ b⊥ ) ≤ (c⊥ ∩ b⊥ )
11	10	lelor 166	. . . . . . 7 ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )) ≤ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))
12	7, 11	le2or 168	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ))) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
13	4, 12	bltr 138	. . . . 5 C (a, b) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
14		df-cmtr 134	. . . . . . 7 C (c, b) = (((c ∩ b) ∪ (c ∩ b⊥ )) ∪ ((c⊥ ∩ b) ∪ (c⊥ ∩ b⊥ )))
15		or4 84	. . . . . . 7 (((c ∩ b) ∪ (c ∩ b⊥ )) ∪ ((c⊥ ∩ b) ∪ (c⊥ ∩ b⊥ ))) = (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
16	14, 15	ax-r2 36	. . . . . 6 C (c, b) = (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
17		lear 161	. . . . . . . 8 (c ∩ b) ≤ b
18		lear 161	. . . . . . . 8 (c⊥ ∩ b) ≤ b
19	17, 18	lel2or 170	. . . . . . 7 ((c ∩ b) ∪ (c⊥ ∩ b)) ≤ b
20	8	leran 153	. . . . . . . 8 (c ∩ b⊥ ) ≤ (a ∩ b⊥ )
21	20	leror 152	. . . . . . 7 ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )) ≤ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))
22	19, 21	le2or 168	. . . . . 6 (((c ∩ b) ∪ (c⊥ ∩ b)) ∪ ((c ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
23	16, 22	bltr 138	. . . . 5 C (c, b) ≤ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
24	13, 23	le2or 168	. . . 4 ( C (a, b) ∪ C (c, b)) ≤ ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
25	1, 24	letr 137	. . 3 c ≤ ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
26		df-i0 43	. . . . 5 ((a →0 b) →0 (c →2 b)) = ((a →0 b)⊥ ∪ (c →2 b))
27		or12 80	. . . . . 6 ((a ∩ b⊥ ) ∪ (b ∪ (c⊥ ∩ b⊥ ))) = (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
28		df-i0 43	. . . . . . . . 9 (a →0 b) = (a⊥ ∪ b)
29	28	ax-r4 37	. . . . . . . 8 (a →0 b)⊥ = (a⊥ ∪ b)⊥
30		anor1 88	. . . . . . . . 9 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
31	30	ax-r1 35	. . . . . . . 8 (a⊥ ∪ b)⊥ = (a ∩ b⊥ )
32	29, 31	ax-r2 36	. . . . . . 7 (a →0 b)⊥ = (a ∩ b⊥ )
33		df-i2 45	. . . . . . 7 (c →2 b) = (b ∪ (c⊥ ∩ b⊥ ))
34	32, 33	2or 72	. . . . . 6 ((a →0 b)⊥ ∪ (c →2 b)) = ((a ∩ b⊥ ) ∪ (b ∪ (c⊥ ∩ b⊥ )))
35		oridm 110	. . . . . 6 ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))) = (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))
36	27, 34, 35	3tr1 63	. . . . 5 ((a →0 b)⊥ ∪ (c →2 b)) = ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
37	26, 36	ax-r2 36	. . . 4 ((a →0 b) →0 (c →2 b)) = ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))))
38	37	ax-r1 35	. . 3 ((b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ ))) ∪ (b ∪ ((a ∩ b⊥ ) ∪ (c⊥ ∩ b⊥ )))) = ((a →0 b) →0 (c →2 b))
39	25, 38	lbtr 139	. 2 c ≤ ((a →0 b) →0 (c →2 b))
40		3vded22.3	. 2 c ≤ (a →0 b)
41	39, 40	3vded21 817	1 c ≤ b

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₀ wi0 11   →₂ wi2 13   C wcmtr 29

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-i0 43  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133  df-cmtr 134

This theorem is referenced by: (None)