Theorem u3lem7 774

Description: Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)

Assertion

Ref	Expression
u3lem7	(a →3 (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))

Proof of Theorem u3lem7

Step	Hyp	Ref	Expression
1		comi31 508	. . . 4 a⊥ C (a⊥ →3 b)
2	1	comcom6 459	. . 3 a C (a⊥ →3 b)
3	2	u3lemc4 703	. 2 (a →3 (a⊥ →3 b)) = (a⊥ ∪ (a⊥ →3 b))
4		df-i3 46	. . . 4 (a⊥ →3 b) = (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))
5	4	lor 70	. . 3 (a⊥ ∪ (a⊥ →3 b)) = (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))))
6		or12 80	. . . 4 (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))))
7		ax-a1 30	. . . . . . . . 9 a = a⊥ ⊥
8	7	ran 78	. . . . . . . 8 (a ∩ b) = (a⊥ ⊥ ∩ b)
9	7	ran 78	. . . . . . . 8 (a ∩ b⊥ ) = (a⊥ ⊥ ∩ b⊥ )
10	8, 9	2or 72	. . . . . . 7 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ ))
11	10	ax-r1 35	. . . . . 6 ((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
12		orabs 120	. . . . . 6 (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))) = a⊥
13	11, 12	2or 72	. . . . 5 (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ )
14		ax-a2 31	. . . . 5 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ ) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
15	13, 14	ax-r2 36	. . . 4 (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
16	6, 15	ax-r2 36	. . 3 (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
17	5, 16	ax-r2 36	. 2 (a⊥ ∪ (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
18	3, 17	ax-r2 36	1 (a →3 (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₃ wi3 14

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

This theorem is used by:  u3lem8  783  u3lem9  784