QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud2lem1 GIF version

Theorem ud2lem1 563
Description: Lemma for unified disjunction. (Contributed by NM, 22-Nov-1997.)
Assertion
Ref Expression
ud2lem1 ((a2 b) →2 (b2 a)) = (a ∪ (ab ))

Proof of Theorem ud2lem1
StepHypRef Expression
1 df-i2 45 . 2 ((a2 b) →2 (b2 a)) = ((b2 a) ∪ ((a2 b) ∩ (b2 a) ))
2 df-i2 45 . . . 4 (b2 a) = (a ∪ (ba ))
3 ud2lem0c 278 . . . . 5 (a2 b) = (b ∩ (ab))
4 ud2lem0c 278 . . . . 5 (b2 a) = (a ∩ (ba))
53, 42an 79 . . . 4 ((a2 b) ∩ (b2 a) ) = ((b ∩ (ab)) ∩ (a ∩ (ba)))
62, 52or 72 . . 3 ((b2 a) ∪ ((a2 b) ∩ (b2 a) )) = ((a ∪ (ba )) ∪ ((b ∩ (ab)) ∩ (a ∩ (ba))))
7 ancom 74 . . . . . 6 (ba ) = (ab )
87lor 70 . . . . 5 (a ∪ (ba )) = (a ∪ (ab ))
9 dff 101 . . . . . . . 8 0 = ((ba ) ∩ (ba ) )
10 oran 87 . . . . . . . . . 10 (ba) = (ba )
1110ax-r1 35 . . . . . . . . 9 (ba ) = (ba)
1211lan 77 . . . . . . . 8 ((ba ) ∩ (ba ) ) = ((ba ) ∩ (ba))
139, 12ax-r2 36 . . . . . . 7 0 = ((ba ) ∩ (ba))
14 anandir 115 . . . . . . . 8 ((ba ) ∩ (ba)) = ((b ∩ (ba)) ∩ (a ∩ (ba)))
15 ax-a2 31 . . . . . . . . . 10 (ba) = (ab)
1615lan 77 . . . . . . . . 9 (b ∩ (ba)) = (b ∩ (ab))
1716ran 78 . . . . . . . 8 ((b ∩ (ba)) ∩ (a ∩ (ba))) = ((b ∩ (ab)) ∩ (a ∩ (ba)))
1814, 17ax-r2 36 . . . . . . 7 ((ba ) ∩ (ba)) = ((b ∩ (ab)) ∩ (a ∩ (ba)))
1913, 18ax-r2 36 . . . . . 6 0 = ((b ∩ (ab)) ∩ (a ∩ (ba)))
2019ax-r1 35 . . . . 5 ((b ∩ (ab)) ∩ (a ∩ (ba))) = 0
218, 202or 72 . . . 4 ((a ∪ (ba )) ∪ ((b ∩ (ab)) ∩ (a ∩ (ba)))) = ((a ∪ (ab )) ∪ 0)
22 or0 102 . . . 4 ((a ∪ (ab )) ∪ 0) = (a ∪ (ab ))
2321, 22ax-r2 36 . . 3 ((a ∪ (ba )) ∪ ((b ∩ (ab)) ∩ (a ∩ (ba)))) = (a ∪ (ab ))
246, 23ax-r2 36 . 2 ((b2 a) ∪ ((a2 b) ∩ (b2 a) )) = (a ∪ (ab ))
251, 24ax-r2 36 1 ((a2 b) →2 (b2 a)) = (a ∪ (ab ))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  2 wi2 13
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i2 45
This theorem is referenced by:  ud2  596
  Copyright terms: Public domain W3C validator