Theorem u3lem7 756

Description: Lemma for unified implication study.

Assertion

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

Proof of Theorem u3lem7

Step	Hyp	Ref	Expression
1		comi31 490	. . . 4 a⊥ C (a⊥ →3 b)
2	1	comcom6 441	. . 3 a C (a⊥ →3 b)
3	2	u3lemc4 685	. 2 (a →3 (a⊥ →3 b)) = (a⊥ ∪ (a⊥ →3 b))
4		df-i3 45	. . . 4 (a⊥ →3 b) = (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))
5	4	lor 66	. . 3 (a⊥ ∪ (a⊥ →3 b)) = (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))))
6		or12 73	. . . 4 (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))))
7		ax-a1 29	. . . . . . . . 9 a = a⊥ ⊥
8	7	ran 71	. . . . . . . 8 (a ∩ b) = (a⊥ ⊥ ∩ b)
9	7	ran 71	. . . . . . . 8 (a ∩ b⊥ ) = (a⊥ ⊥ ∩ b⊥ )
10	8, 9	2or 67	. . . . . . 7 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ ))
11	10	ax-r1 34	. . . . . 6 ((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
12		a5b 112	. . . . . 6 (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b))) = a⊥
13	11, 12	2or 67	. . . . 5 (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ )
14		ax-a2 30	. . . . 5 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ ) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
15	13, 14	ax-r2 35	. . . 4 (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
16	6, 15	ax-r2 35	. . 3 (a⊥ ∪ (((a⊥ ⊥ ∩ b) ∪ (a⊥ ⊥ ∩ b⊥ )) ∪ (a⊥ ∩ (a⊥ ⊥ ∪ b)))) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
17	5, 16	ax-r2 35	. 2 (a⊥ ∪ (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
18	3, 17	ax-r2 35	1 (a →3 (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₃ wi3 15

This theorem is referenced by:  u3lem8 765  u3lem9 766

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

metamath.org