Theorem u1lem11 762

Description: Lemma used in study of orthoarguesian law.

Assertion

Ref	Expression
u1lem11	((a_|_ ->1 b) ->1 b) = (a ->1 b)

Proof of Theorem u1lem11

Step	Hyp	Ref	Expression
1		ud1lem0c 269	. . . . 5 (a_|_ ->1 b)_|_ = (a_|_ ^ (a_|__|_ v b_|_))
2		ax-a1 29	. . . . . . . 8 a = a_|__|_
3	2	ax-r1 34	. . . . . . 7 a_|__|_ = a
4	3	ax-r5 37	. . . . . 6 (a_|__|_ v b_|_) = (a v b_|_)
5	4	lan 70	. . . . 5 (a_|_ ^ (a_|__|_ v b_|_)) = (a_|_ ^ (a v b_|_))
6	1, 5	ax-r2 35	. . . 4 (a_|_ ->1 b)_|_ = (a_|_ ^ (a v b_|_))
7		u1lemab 592	. . . . 5 ((a_|_ ->1 b) ^ b) = ((a_|_ ^ b) v (a_|__|_ ^ b))
8		ax-a2 30	. . . . 5 ((a_|_ ^ b) v (a_|__|_ ^ b)) = ((a_|__|_ ^ b) v (a_|_ ^ b))
9	2	ran 71	. . . . . . 7 (a ^ b) = (a_|__|_ ^ b)
10	9	ax-r5 37	. . . . . 6 ((a ^ b) v (a_|_ ^ b)) = ((a_|__|_ ^ b) v (a_|_ ^ b))
11	10	ax-r1 34	. . . . 5 ((a_|__|_ ^ b) v (a_|_ ^ b)) = ((a ^ b) v (a_|_ ^ b))
12	7, 8, 11	3tr 62	. . . 4 ((a_|_ ->1 b) ^ b) = ((a ^ b) v (a_|_ ^ b))
13	6, 12	2or 67	. . 3 ((a_|_ ->1 b)_|_ v ((a_|_ ->1 b) ^ b)) = ((a_|_ ^ (a v b_|_)) v ((a ^ b) v (a_|_ ^ b)))
14		comanr1 446	. . . . . . 7 a C (a ^ b)
15	14	comcom3 436	. . . . . 6 a_|_ C (a ^ b)
16		comanr1 446	. . . . . 6 a_|_ C (a_|_ ^ b)
17	15, 16	com2or 465	. . . . 5 a_|_ C ((a ^ b) v (a_|_ ^ b))
18	17	comcom 435	. . . 4 ((a ^ b) v (a_|_ ^ b)) C a_|_
19		comor1 443	. . . . . . 7 (a v b_|_) C a
20		comor2 444	. . . . . . . 8 (a v b_|_) C b_|_
21	20	comcom7 442	. . . . . . 7 (a v b_|_) C b
22	19, 21	com2an 466	. . . . . 6 (a v b_|_) C (a ^ b)
23	19	comcom2 175	. . . . . . 7 (a v b_|_) C a_|_
24	23, 21	com2an 466	. . . . . 6 (a v b_|_) C (a_|_ ^ b)
25	22, 24	com2or 465	. . . . 5 (a v b_|_) C ((a ^ b) v (a_|_ ^ b))
26	25	comcom 435	. . . 4 ((a ^ b) v (a_|_ ^ b)) C (a v b_|_)
27	18, 26	fh3r 457	. . 3 ((a_|_ ^ (a v b_|_)) v ((a ^ b) v (a_|_ ^ b))) = ((a_|_ v ((a ^ b) v (a_|_ ^ b))) ^ ((a v b_|_) v ((a ^ b) v (a_|_ ^ b))))
28		or32 75	. . . . . 6 ((a_|_ v (a ^ b)) v (a_|_ ^ b)) = ((a_|_ v (a_|_ ^ b)) v (a ^ b))
29		ax-a3 31	. . . . . 6 ((a_|_ v (a ^ b)) v (a_|_ ^ b)) = (a_|_ v ((a ^ b) v (a_|_ ^ b)))
30		a5b 112	. . . . . . 7 (a_|_ v (a_|_ ^ b)) = a_|_
31	30	ax-r5 37	. . . . . 6 ((a_|_ v (a_|_ ^ b)) v (a ^ b)) = (a_|_ v (a ^ b))
32	28, 29, 31	3tr2 61	. . . . 5 (a_|_ v ((a ^ b) v (a_|_ ^ b))) = (a_|_ v (a ^ b))
33		or12 73	. . . . . 6 ((a v b_|_) v ((a ^ b) v (a_|_ ^ b))) = ((a ^ b) v ((a v b_|_) v (a_|_ ^ b)))
34		anor2 81	. . . . . . . . 9 (a_|_ ^ b) = (a v b_|_)_|_
35	34	lor 66	. . . . . . . 8 ((a v b_|_) v (a_|_ ^ b)) = ((a v b_|_) v (a v b_|_)_|_)
36		df-t 40	. . . . . . . . 9 1 = ((a v b_|_) v (a v b_|_)_|_)
37	36	ax-r1 34	. . . . . . . 8 ((a v b_|_) v (a v b_|_)_|_) = 1
38	35, 37	ax-r2 35	. . . . . . 7 ((a v b_|_) v (a_|_ ^ b)) = 1
39	38	lor 66	. . . . . 6 ((a ^ b) v ((a v b_|_) v (a_|_ ^ b))) = ((a ^ b) v 1)
40		or1 96	. . . . . 6 ((a ^ b) v 1) = 1
41	33, 39, 40	3tr 62	. . . . 5 ((a v b_|_) v ((a ^ b) v (a_|_ ^ b))) = 1
42	32, 41	2an 72	. . . 4 ((a_|_ v ((a ^ b) v (a_|_ ^ b))) ^ ((a v b_|_) v ((a ^ b) v (a_|_ ^ b)))) = ((a_|_ v (a ^ b)) ^ 1)
43		an1 98	. . . 4 ((a_|_ v (a ^ b)) ^ 1) = (a_|_ v (a ^ b))
44	42, 43	ax-r2 35	. . 3 ((a_|_ v ((a ^ b) v (a_|_ ^ b))) ^ ((a v b_|_) v ((a ^ b) v (a_|_ ^ b)))) = (a_|_ v (a ^ b))
45	13, 27, 44	3tr 62	. 2 ((a_|_ ->1 b)_|_ v ((a_|_ ->1 b) ^ b)) = (a_|_ v (a ^ b))
46		df-i1 43	. 2 ((a_|_ ->1 b) ->1 b) = ((a_|_ ->1 b)_|_ v ((a_|_ ->1 b) ^ b))
47		df-i1 43	. 2 (a ->1 b) = (a_|_ v (a ^ b))
48	45, 46, 47	3tr1 60	1 ((a_|_ ->1 b) ->1 b) = (a ->1 b)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13

This theorem is referenced by:  u1lem12 763  2oai1u 804  1oath1i1u 810  oa4to4u 953  3oa2 1004

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-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org