QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud5lem1 Unicode version
Theorem ud5lem1 589
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud5lem1 ((a ->5 b) ->5 (b ->5 a)) = (a v b')
Proof of Theorem ud5lem1
StepHypRef Expression
1 df-i5 48 . 2 ((a ->5 b) ->5 (b ->5 a)) = ((((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) v ((a ->5 b)' ^ (b ->5 a)'))
2 ud5lem1a 586 . . . . 5 ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
3 ud5lem1b 587 . . . . 5 ((a ->5 b)' ^ (b ->5 a)) = (a ^ b')
42, 32or 72 . . . 4 (((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) = (((a ^ b) v (a' ^ b')) v (a ^ b'))
5 ud5lem1c 588 . . . 4 ((a ->5 b)' ^ (b ->5 a)') = (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))
64, 52or 72 . . 3 ((((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) v ((a ->5 b)' ^ (b ->5 a)')) = ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b'))))
7 coman1 185 . . . . . . . . . 10 (a ^ b) C a
8 coman2 186 . . . . . . . . . 10 (a ^ b) C b
97, 8com2or 483 . . . . . . . . 9 (a ^ b) C (a v b)
108comcom2 183 . . . . . . . . . 10 (a ^ b) C b'
117, 10com2or 483 . . . . . . . . 9 (a ^ b) C (a v b')
129, 11com2an 484 . . . . . . . 8 (a ^ b) C ((a v b) ^ (a v b'))
1312comcom 453 . . . . . . 7 ((a v b) ^ (a v b')) C (a ^ b)
14 coman1 185 . . . . . . . . . . 11 (a' ^ b') C a'
1514comcom7 460 . . . . . . . . . 10 (a' ^ b') C a
16 coman2 186 . . . . . . . . . . 11 (a' ^ b') C b'
1716comcom7 460 . . . . . . . . . 10 (a' ^ b') C b
1815, 17com2or 483 . . . . . . . . 9 (a' ^ b') C (a v b)
1915, 16com2or 483 . . . . . . . . 9 (a' ^ b') C (a v b')
2018, 19com2an 484 . . . . . . . 8 (a' ^ b') C ((a v b) ^ (a v b'))
2120comcom 453 . . . . . . 7 ((a v b) ^ (a v b')) C (a' ^ b')
2213, 21com2or 483 . . . . . 6 ((a v b) ^ (a v b')) C ((a ^ b) v (a' ^ b'))
23 coman1 185 . . . . . . . . 9 (a ^ b') C a
24 coman2 186 . . . . . . . . . 10 (a ^ b') C b'
2524comcom7 460 . . . . . . . . 9 (a ^ b') C b
2623, 25com2or 483 . . . . . . . 8 (a ^ b') C (a v b)
2723, 24com2or 483 . . . . . . . 8 (a ^ b') C (a v b')
2826, 27com2an 484 . . . . . . 7 (a ^ b') C ((a v b) ^ (a v b'))
2928comcom 453 . . . . . 6 ((a v b) ^ (a v b')) C (a ^ b')
3022, 29com2or 483 . . . . 5 ((a v b) ^ (a v b')) C (((a ^ b) v (a' ^ b')) v (a ^ b'))
31 comor1 461 . . . . . . . . . 10 (a' v b) C a'
3231comcom7 460 . . . . . . . . 9 (a' v b) C a
33 comor2 462 . . . . . . . . 9 (a' v b) C b
3432, 33com2or 483 . . . . . . . 8 (a' v b) C (a v b)
3533comcom2 183 . . . . . . . . 9 (a' v b) C b'
3632, 35com2or 483 . . . . . . . 8 (a' v b) C (a v b')
3734, 36com2an 484 . . . . . . 7 (a' v b) C ((a v b) ^ (a v b'))
3837comcom 453 . . . . . 6 ((a v b) ^ (a v b')) C (a' v b)
39 comor1 461 . . . . . . . . . 10 (a' v b') C a'
4039comcom7 460 . . . . . . . . 9 (a' v b') C a
41 comor2 462 . . . . . . . . . 10 (a' v b') C b'
4241comcom7 460 . . . . . . . . 9 (a' v b') C b
4340, 42com2or 483 . . . . . . . 8 (a' v b') C (a v b)
4440, 41com2or 483 . . . . . . . 8 (a' v b') C (a v b')
4543, 44com2an 484 . . . . . . 7 (a' v b') C ((a v b) ^ (a v b'))
4645comcom 453 . . . . . 6 ((a v b) ^ (a v b')) C (a' v b')
4738, 46com2an 484 . . . . 5 ((a v b) ^ (a v b')) C ((a' v b) ^ (a' v b'))
4830, 47fh4 472 . . . 4 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))) = (((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b'))))
49 comor1 461 . . . . . . . . . . 11 (a v b) C a
50 comor2 462 . . . . . . . . . . 11 (a v b) C b
5149, 50com2an 484 . . . . . . . . . 10 (a v b) C (a ^ b)
5249comcom2 183 . . . . . . . . . . 11 (a v b) C a'
5350comcom2 183 . . . . . . . . . . 11 (a v b) C b'
5452, 53com2an 484 . . . . . . . . . 10 (a v b) C (a' ^ b')
5551, 54com2or 483 . . . . . . . . 9 (a v b) C ((a ^ b) v (a' ^ b'))
5649, 53com2an 484 . . . . . . . . 9 (a v b) C (a ^ b')
5755, 56com2or 483 . . . . . . . 8 (a v b) C (((a ^ b) v (a' ^ b')) v (a ^ b'))
5849, 53com2or 483 . . . . . . . 8 (a v b) C (a v b')
5957, 58fh4 472 . . . . . . 7 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) = (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b')))
60 or32 82 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) = ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b'))
61 ax-a3 32 . . . . . . . . . . . . 13 (((a ^ b) v (a' ^ b')) v (a v b)) = ((a ^ b) v ((a' ^ b') v (a v b)))
62 oran 87 . . . . . . . . . . . . . . . . 17 (a v b) = (a' ^ b')'
6362lor 70 . . . . . . . . . . . . . . . 16 ((a' ^ b') v (a v b)) = ((a' ^ b') v (a' ^ b')')
64 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a' ^ b') v (a' ^ b')')
6564ax-r1 35 . . . . . . . . . . . . . . . 16 ((a' ^ b') v (a' ^ b')') = 1
6663, 65ax-r2 36 . . . . . . . . . . . . . . 15 ((a' ^ b') v (a v b)) = 1
6766lor 70 . . . . . . . . . . . . . 14 ((a ^ b) v ((a' ^ b') v (a v b))) = ((a ^ b) v 1)
68 or1 104 . . . . . . . . . . . . . 14 ((a ^ b) v 1) = 1
6967, 68ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b) v ((a' ^ b') v (a v b))) = 1
7061, 69ax-r2 36 . . . . . . . . . . . 12 (((a ^ b) v (a' ^ b')) v (a v b)) = 1
7170ax-r5 38 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b')) = (1 v (a ^ b'))
72 or1r 105 . . . . . . . . . . 11 (1 v (a ^ b')) = 1
7371, 72ax-r2 36 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b')) = 1
7460, 73ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) = 1
75 lea 160 . . . . . . . . . . . . 13 (a ^ b) =< a
76 leo 158 . . . . . . . . . . . . 13 a =< (a v b')
7775, 76letr 137 . . . . . . . . . . . 12 (a ^ b) =< (a v b')
78 lear 161 . . . . . . . . . . . . 13 (a' ^ b') =< b'
79 leor 159 . . . . . . . . . . . . 13 b' =< (a v b')
8078, 79letr 137 . . . . . . . . . . . 12 (a' ^ b') =< (a v b')
8177, 80lel2or 170 . . . . . . . . . . 11 ((a ^ b) v (a' ^ b')) =< (a v b')
82 lea 160 . . . . . . . . . . . 12 (a ^ b') =< a
8382, 76letr 137 . . . . . . . . . . 11 (a ^ b') =< (a v b')
8481, 83lel2or 170 . . . . . . . . . 10 (((a ^ b) v (a' ^ b')) v (a ^ b')) =< (a v b')
8584df-le2 131 . . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b')) = (a v b')
8674, 852an 79 . . . . . . . 8 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b'))) = (1 ^ (a v b'))
87 an1r 107 . . . . . . . 8 (1 ^ (a v b')) = (a v b')
8886, 87ax-r2 36 . . . . . . 7 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b'))) = (a v b')
8959, 88ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) = (a v b')
9032, 33com2an 484 . . . . . . . . . 10 (a' v b) C (a ^ b)
9131, 35com2an 484 . . . . . . . . . 10 (a' v b) C (a' ^ b')
9290, 91com2or 483 . . . . . . . . 9 (a' v b) C ((a ^ b) v (a' ^ b'))
9332, 35com2an 484 . . . . . . . . 9 (a' v b) C (a ^ b')
9492, 93com2or 483 . . . . . . . 8 (a' v b) C (((a ^ b) v (a' ^ b')) v (a ^ b'))
9531, 35com2or 483 . . . . . . . 8 (a' v b) C (a' v b')
9694, 95fh4 472 . . . . . . 7 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b'))) = (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b')))
97 ax-a3 32 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b)) = (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' v b)))
98 anor1 88 . . . . . . . . . . . . . . . 16 (a ^ b') = (a' v b)'
9998ax-r1 35 . . . . . . . . . . . . . . 15 (a' v b)' = (a ^ b')
10099con3 68 . . . . . . . . . . . . . 14 (a' v b) = (a ^ b')'
101100lor 70 . . . . . . . . . . . . 13 ((a ^ b') v (a' v b)) = ((a ^ b') v (a ^ b')')
102 df-t 41 . . . . . . . . . . . . . 14 1 = ((a ^ b') v (a ^ b')')
103102ax-r1 35 . . . . . . . . . . . . 13 ((a ^ b') v (a ^ b')') = 1
104101, 103ax-r2 36 . . . . . . . . . . . 12 ((a ^ b') v (a' v b)) = 1
105104lor 70 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' v b))) = (((a ^ b) v (a' ^ b')) v 1)
106 or1 104 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b')) v 1) = 1
107105, 106ax-r2 36 . . . . . . . . . 10 (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' v b))) = 1
10897, 107ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b)) = 1
109 or32 82 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b')) = ((((a ^ b) v (a' ^ b')) v (a' v b')) v (a ^ b'))
110 or32 82 . . . . . . . . . . . . 13 (((a ^ b) v (a' ^ b')) v (a' v b')) = (((a ^ b) v (a' v b')) v (a' ^ b'))
111 df-a 40 . . . . . . . . . . . . . . . . . . 19 (a ^ b) = (a' v b')'
112111ax-r1 35 . . . . . . . . . . . . . . . . . 18 (a' v b')' = (a ^ b)
113112con3 68 . . . . . . . . . . . . . . . . 17 (a' v b') = (a ^ b)'
114113lor 70 . . . . . . . . . . . . . . . 16 ((a ^ b) v (a' v b')) = ((a ^ b) v (a ^ b)')
115 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a ^ b) v (a ^ b)')
116115ax-r1 35 . . . . . . . . . . . . . . . 16 ((a ^ b) v (a ^ b)') = 1
117114, 116ax-r2 36 . . . . . . . . . . . . . . 15 ((a ^ b) v (a' v b')) = 1
118117ax-r5 38 . . . . . . . . . . . . . 14 (((a ^ b) v (a' v b')) v (a' ^ b')) = (1 v (a' ^ b'))
119 or1r 105 . . . . . . . . . . . . . 14 (1 v (a' ^ b')) = 1
120118, 119ax-r2 36 . . . . . . . . . . . . 13 (((a ^ b) v (a' v b')) v (a' ^ b')) = 1
121110, 120ax-r2 36 . . . . . . . . . . . 12 (((a ^ b) v (a' ^ b')) v (a' v b')) = 1
122121ax-r5 38 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b')) v (a' v b')) v (a ^ b')) = (1 v (a ^ b'))
123122, 72ax-r2 36 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a' v b')) v (a ^ b')) = 1
124109, 123ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b')) = 1
125108, 1242an 79 . . . . . . . 8 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b'))) = (1 ^ 1)
126 an1 106 . . . . . . . 8 (1 ^ 1) = 1
127125, 126ax-r2 36 . . . . . . 7 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a' v b'))) = 1
12896, 127ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b'))) = 1
12989, 1282an 79 . . . . 5 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b')))) = ((a v b') ^ 1)
130 an1 106 . . . . 5 ((a v b') ^ 1) = (a v b')
131129, 130ax-r2 36 . . . 4 (((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b')))) = (a v b')
13248, 131ax-r2 36 . . 3 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))) = (a v b')
1336, 132ax-r2 36 . 2 ((((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) v ((a ->5 b)' ^ (b ->5 a)')) = (a v b')
1341, 133ax-r2 36 1 ((a ->5 b) ->5 (b ->5 a)) = (a v b')
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->5 wi5 16
This theorem was proved from 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 theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud5  599
  Copyright terms: Public domain W3C validator