Theorem lem4.6.7 1103

Description: Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-2005.)

Hypothesis

Ref	Expression
lem4.6.7.1	a⊥ ≤ b

Assertion

Ref	Expression
lem4.6.7	b ≤ (a →1 b)

Proof of Theorem lem4.6.7

Step	Hyp	Ref	Expression
1		leid 148	. . . . . . 7 a ≤ a
2	1	sklem 230	. . . . . 6 (a⊥ ∪ a) = 1
3	2	ax-r1 35	. . . . 5 1 = (a⊥ ∪ a)
4		lem4.6.7.1	. . . . . . 7 a⊥ ≤ b
5	4	df-le2 131	. . . . . 6 (a⊥ ∪ b) = b
6	5	ax-r1 35	. . . . 5 b = (a⊥ ∪ b)
7	3, 6	2an 79	. . . 4 (1 ∩ b) = ((a⊥ ∪ a) ∩ (a⊥ ∪ b))
8		ax-a3 32	. . . . . 6 ((b ∪ a⊥ ) ∪ (a ∩ b)) = (b ∪ (a⊥ ∪ (a ∩ b)))
9	8	ax-r1 35	. . . . 5 (b ∪ (a⊥ ∪ (a ∩ b))) = ((b ∪ a⊥ ) ∪ (a ∩ b))
10		le1 146	. . . . . . . . 9 b ≤ 1
11		leid 148	. . . . . . . . 9 b ≤ b
12	10, 11	ler2an 173	. . . . . . . 8 b ≤ (1 ∩ b)
13		le1 146	. . . . . . . . 9 a⊥ ≤ 1
14	13, 4	ler2an 173	. . . . . . . 8 a⊥ ≤ (1 ∩ b)
15	12, 14	lel2or 170	. . . . . . 7 (b ∪ a⊥ ) ≤ (1 ∩ b)
16		le1 146	. . . . . . . 8 a ≤ 1
17	16	leran 153	. . . . . . 7 (a ∩ b) ≤ (1 ∩ b)
18	15, 17	lel2or 170	. . . . . 6 ((b ∪ a⊥ ) ∪ (a ∩ b)) ≤ (1 ∩ b)
19		leao2 163	. . . . . . 7 (1 ∩ b) ≤ (b ∪ a⊥ )
20	19	ler 149	. . . . . 6 (1 ∩ b) ≤ ((b ∪ a⊥ ) ∪ (a ∩ b))
21	18, 20	lebi 145	. . . . 5 ((b ∪ a⊥ ) ∪ (a ∩ b)) = (1 ∩ b)
22	9, 21	ax-r2 36	. . . 4 (b ∪ (a⊥ ∪ (a ∩ b))) = (1 ∩ b)
23		comid 187	. . . . . 6 a C a
24	23	comcom3 454	. . . . 5 a⊥ C a
25	4	lecom 180	. . . . 5 a⊥ C b
26	24, 25	fh3 471	. . . 4 (a⊥ ∪ (a ∩ b)) = ((a⊥ ∪ a) ∩ (a⊥ ∪ b))
27	7, 22, 26	3tr1 63	. . 3 (b ∪ (a⊥ ∪ (a ∩ b))) = (a⊥ ∪ (a ∩ b))
28	27	df-le1 130	. 2 b ≤ (a⊥ ∪ (a ∩ b))
29		df-i1 44	. . 3 (a →1 b) = (a⊥ ∪ (a ∩ b))
30	29	ax-r1 35	. 2 (a⊥ ∪ (a ∩ b)) = (a →1 b)
31	28, 30	lbtr 139	1 b ≤ (a →1 b)

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12

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-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)