QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud3lem1c Unicode version
Theorem ud3lem1c 568
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud3lem1c ((a ->3 b)' v (b ->3 a)) = (a v b')
Proof of Theorem ud3lem1c
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
2 df-i3 46 . . 3 (b ->3 a) = (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
31, 22or 72 . 2 ((a ->3 b)' v (b ->3 a)) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))
4 coman2 186 . . . . . . . . 9 (b' ^ a) C a
5 coman1 185 . . . . . . . . 9 (b' ^ a) C b'
64, 5com2or 483 . . . . . . . 8 (b' ^ a) C (a v b')
75comcom7 460 . . . . . . . . 9 (b' ^ a) C b
84, 7com2or 483 . . . . . . . 8 (b' ^ a) C (a v b)
96, 8com2an 484 . . . . . . 7 (b' ^ a) C ((a v b') ^ (a v b))
109comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C (b' ^ a)
11 coman2 186 . . . . . . . . . 10 (b' ^ a') C a'
1211comcom7 460 . . . . . . . . 9 (b' ^ a') C a
13 coman1 185 . . . . . . . . 9 (b' ^ a') C b'
1412, 13com2or 483 . . . . . . . 8 (b' ^ a') C (a v b')
1513comcom7 460 . . . . . . . . 9 (b' ^ a') C b
1612, 15com2or 483 . . . . . . . 8 (b' ^ a') C (a v b)
1714, 16com2an 484 . . . . . . 7 (b' ^ a') C ((a v b') ^ (a v b))
1817comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C (b' ^ a')
1910, 18com2or 483 . . . . 5 ((a v b') ^ (a v b)) C ((b' ^ a) v (b' ^ a'))
20 comorr2 463 . . . . . . . . 9 b' C (a v b')
2120comcom6 459 . . . . . . . 8 b C (a v b')
22 comorr2 463 . . . . . . . 8 b C (a v b)
2321, 22com2an 484 . . . . . . 7 b C ((a v b') ^ (a v b))
2423comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C b
25 comor2 462 . . . . . . . . 9 (b' v a) C a
26 comor1 461 . . . . . . . . 9 (b' v a) C b'
2725, 26com2or 483 . . . . . . . 8 (b' v a) C (a v b')
2826comcom7 460 . . . . . . . . 9 (b' v a) C b
2925, 28com2or 483 . . . . . . . 8 (b' v a) C (a v b)
3027, 29com2an 484 . . . . . . 7 (b' v a) C ((a v b') ^ (a v b))
3130comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C (b' v a)
3224, 31com2an 484 . . . . 5 ((a v b') ^ (a v b)) C (b ^ (b' v a))
3319, 32com2or 483 . . . 4 ((a v b') ^ (a v b)) C (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
34 comorr 184 . . . . . . . 8 a C (a v b')
3534comcom3 454 . . . . . . 7 a' C (a v b')
36 comorr 184 . . . . . . . 8 a C (a v b)
3736comcom3 454 . . . . . . 7 a' C (a v b)
3835, 37com2an 484 . . . . . 6 a' C ((a v b') ^ (a v b))
3938comcom 453 . . . . 5 ((a v b') ^ (a v b)) C a'
40 coman1 185 . . . . . . . 8 (a ^ b') C a
41 coman2 186 . . . . . . . 8 (a ^ b') C b'
4240, 41com2or 483 . . . . . . 7 (a ^ b') C (a v b')
4341comcom7 460 . . . . . . . 8 (a ^ b') C b
4440, 43com2or 483 . . . . . . 7 (a ^ b') C (a v b)
4542, 44com2an 484 . . . . . 6 (a ^ b') C ((a v b') ^ (a v b))
4645comcom 453 . . . . 5 ((a v b') ^ (a v b)) C (a ^ b')
4739, 46com2or 483 . . . 4 ((a v b') ^ (a v b)) C (a' v (a ^ b'))
4833, 47fh4r 476 . . 3 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = ((((a v b') ^ (a v b)) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a' v (a ^ b')) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))))
49 comor2 462 . . . . . . . . . 10 (a v b') C b'
50 comor1 461 . . . . . . . . . 10 (a v b') C a
5149, 50com2an 484 . . . . . . . . 9 (a v b') C (b' ^ a)
5250comcom2 183 . . . . . . . . . 10 (a v b') C a'
5349, 52com2an 484 . . . . . . . . 9 (a v b') C (b' ^ a')
5451, 53com2or 483 . . . . . . . 8 (a v b') C ((b' ^ a) v (b' ^ a'))
5549comcom7 460 . . . . . . . . 9 (a v b') C b
5649, 50com2or 483 . . . . . . . . 9 (a v b') C (b' v a)
5755, 56com2an 484 . . . . . . . 8 (a v b') C (b ^ (b' v a))
5854, 57com2or 483 . . . . . . 7 (a v b') C (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
5950, 55com2or 483 . . . . . . 7 (a v b') C (a v b)
6058, 59fh4r 476 . . . . . 6 (((a v b') ^ (a v b)) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (((a v b') v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a v b) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))))
61 ax-a2 31 . . . . . . . . 9 ((a v b') v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = ((((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))) v (a v b'))
62 lea 160 . . . . . . . . . . . . 13 (b' ^ a) =< b'
63 lea 160 . . . . . . . . . . . . 13 (b' ^ a') =< b'
6462, 63lel2or 170 . . . . . . . . . . . 12 ((b' ^ a) v (b' ^ a')) =< b'
65 leor 159 . . . . . . . . . . . 12 b' =< (a v b')
6664, 65letr 137 . . . . . . . . . . 11 ((b' ^ a) v (b' ^ a')) =< (a v b')
67 lear 161 . . . . . . . . . . . 12 (b ^ (b' v a)) =< (b' v a)
68 ax-a2 31 . . . . . . . . . . . 12 (b' v a) = (a v b')
6967, 68lbtr 139 . . . . . . . . . . 11 (b ^ (b' v a)) =< (a v b')
7066, 69lel2or 170 . . . . . . . . . 10 (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))) =< (a v b')
7170df-le2 131 . . . . . . . . 9 ((((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))) v (a v b')) = (a v b')
7261, 71ax-r2 36 . . . . . . . 8 ((a v b') v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (a v b')
73 or12 80 . . . . . . . . 9 ((a v b) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (((b' ^ a) v (b' ^ a')) v ((a v b) v (b ^ (b' v a))))
74 ax-a3 32 . . . . . . . . . . 11 ((((b' ^ a) v (b' ^ a')) v (a v b)) v (b ^ (b' v a))) = (((b' ^ a) v (b' ^ a')) v ((a v b) v (b ^ (b' v a))))
7574ax-r1 35 . . . . . . . . . 10 (((b' ^ a) v (b' ^ a')) v ((a v b) v (b ^ (b' v a)))) = ((((b' ^ a) v (b' ^ a')) v (a v b)) v (b ^ (b' v a)))
76 ax-a3 32 . . . . . . . . . . . . 13 (((b' ^ a) v (b' ^ a')) v (a v b)) = ((b' ^ a) v ((b' ^ a') v (a v b)))
77 ancom 74 . . . . . . . . . . . . . . . . 17 (b' ^ a') = (a' ^ b')
78 oran 87 . . . . . . . . . . . . . . . . 17 (a v b) = (a' ^ b')'
7977, 782or 72 . . . . . . . . . . . . . . . 16 ((b' ^ a') v (a v b)) = ((a' ^ b') v (a' ^ b')')
80 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a' ^ b') v (a' ^ b')')
8180ax-r1 35 . . . . . . . . . . . . . . . 16 ((a' ^ b') v (a' ^ b')') = 1
8279, 81ax-r2 36 . . . . . . . . . . . . . . 15 ((b' ^ a') v (a v b)) = 1
8382lor 70 . . . . . . . . . . . . . 14 ((b' ^ a) v ((b' ^ a') v (a v b))) = ((b' ^ a) v 1)
84 or1 104 . . . . . . . . . . . . . 14 ((b' ^ a) v 1) = 1
8583, 84ax-r2 36 . . . . . . . . . . . . 13 ((b' ^ a) v ((b' ^ a') v (a v b))) = 1
8676, 85ax-r2 36 . . . . . . . . . . . 12 (((b' ^ a) v (b' ^ a')) v (a v b)) = 1
8786ax-r5 38 . . . . . . . . . . 11 ((((b' ^ a) v (b' ^ a')) v (a v b)) v (b ^ (b' v a))) = (1 v (b ^ (b' v a)))
88 or1r 105 . . . . . . . . . . 11 (1 v (b ^ (b' v a))) = 1
8987, 88ax-r2 36 . . . . . . . . . 10 ((((b' ^ a) v (b' ^ a')) v (a v b)) v (b ^ (b' v a))) = 1
9075, 89ax-r2 36 . . . . . . . . 9 (((b' ^ a) v (b' ^ a')) v ((a v b) v (b ^ (b' v a)))) = 1
9173, 90ax-r2 36 . . . . . . . 8 ((a v b) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = 1
9272, 912an 79 . . . . . . 7 (((a v b') v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a v b) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))) = ((a v b') ^ 1)
93 an1 106 . . . . . . 7 ((a v b') ^ 1) = (a v b')
9492, 93ax-r2 36 . . . . . 6 (((a v b') v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a v b) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))) = (a v b')
9560, 94ax-r2 36 . . . . 5 (((a v b') ^ (a v b)) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (a v b')
96 or12 80 . . . . . 6 ((a' v (a ^ b')) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (((b' ^ a) v (b' ^ a')) v ((a' v (a ^ b')) v (b ^ (b' v a))))
97 ax-a2 31 . . . . . . . . . 10 (a' v (a ^ b')) = ((a ^ b') v a')
98 ancom 74 . . . . . . . . . 10 (b ^ (b' v a)) = ((b' v a) ^ b)
9997, 982or 72 . . . . . . . . 9 ((a' v (a ^ b')) v (b ^ (b' v a))) = (((a ^ b') v a') v ((b' v a) ^ b))
100 ax-a3 32 . . . . . . . . . 10 (((a ^ b') v a') v ((b' v a) ^ b)) = ((a ^ b') v (a' v ((b' v a) ^ b)))
10125comcom2 183 . . . . . . . . . . . . . 14 (b' v a) C a'
102101, 28fh4 472 . . . . . . . . . . . . 13 (a' v ((b' v a) ^ b)) = ((a' v (b' v a)) ^ (a' v b))
103 ax-a2 31 . . . . . . . . . . . . . . . 16 (a' v (b' v a)) = ((b' v a) v a')
104 ax-a3 32 . . . . . . . . . . . . . . . . 17 ((b' v a) v a') = (b' v (a v a'))
105 df-t 41 . . . . . . . . . . . . . . . . . . . 20 1 = (a v a')
106105ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (a v a') = 1
107106lor 70 . . . . . . . . . . . . . . . . . 18 (b' v (a v a')) = (b' v 1)
108 or1 104 . . . . . . . . . . . . . . . . . 18 (b' v 1) = 1
109107, 108ax-r2 36 . . . . . . . . . . . . . . . . 17 (b' v (a v a')) = 1
110104, 109ax-r2 36 . . . . . . . . . . . . . . . 16 ((b' v a) v a') = 1
111103, 110ax-r2 36 . . . . . . . . . . . . . . 15 (a' v (b' v a)) = 1
112111ran 78 . . . . . . . . . . . . . 14 ((a' v (b' v a)) ^ (a' v b)) = (1 ^ (a' v b))
113 an1r 107 . . . . . . . . . . . . . 14 (1 ^ (a' v b)) = (a' v b)
114112, 113ax-r2 36 . . . . . . . . . . . . 13 ((a' v (b' v a)) ^ (a' v b)) = (a' v b)
115102, 114ax-r2 36 . . . . . . . . . . . 12 (a' v ((b' v a) ^ b)) = (a' v b)
116115lor 70 . . . . . . . . . . 11 ((a ^ b') v (a' v ((b' v a) ^ b))) = ((a ^ b') v (a' v b))
117 ax-a2 31 . . . . . . . . . . . 12 ((a ^ b') v (a' v b)) = ((a' v b) v (a ^ b'))
118 anor1 88 . . . . . . . . . . . . . 14 (a ^ b') = (a' v b)'
119118lor 70 . . . . . . . . . . . . 13 ((a' v b) v (a ^ b')) = ((a' v b) v (a' v b)')
120 df-t 41 . . . . . . . . . . . . . 14 1 = ((a' v b) v (a' v b)')
121120ax-r1 35 . . . . . . . . . . . . 13 ((a' v b) v (a' v b)') = 1
122119, 121ax-r2 36 . . . . . . . . . . . 12 ((a' v b) v (a ^ b')) = 1
123117, 122ax-r2 36 . . . . . . . . . . 11 ((a ^ b') v (a' v b)) = 1
124116, 123ax-r2 36 . . . . . . . . . 10 ((a ^ b') v (a' v ((b' v a) ^ b))) = 1
125100, 124ax-r2 36 . . . . . . . . 9 (((a ^ b') v a') v ((b' v a) ^ b)) = 1
12699, 125ax-r2 36 . . . . . . . 8 ((a' v (a ^ b')) v (b ^ (b' v a))) = 1
127126lor 70 . . . . . . 7 (((b' ^ a) v (b' ^ a')) v ((a' v (a ^ b')) v (b ^ (b' v a)))) = (((b' ^ a) v (b' ^ a')) v 1)
128 or1 104 . . . . . . 7 (((b' ^ a) v (b' ^ a')) v 1) = 1
129127, 128ax-r2 36 . . . . . 6 (((b' ^ a) v (b' ^ a')) v ((a' v (a ^ b')) v (b ^ (b' v a)))) = 1
13096, 129ax-r2 36 . . . . 5 ((a' v (a ^ b')) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = 1
13195, 1302an 79 . . . 4 ((((a v b') ^ (a v b)) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a' v (a ^ b')) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))) = ((a v b') ^ 1)
132131, 93ax-r2 36 . . 3 ((((a v b') ^ (a v b)) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) ^ ((a' v (a ^ b')) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))) = (a v b')
13348, 132ax-r2 36 . 2 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (a v b')
1343, 133ax-r2 36 1 ((a ->3 b)' v (b ->3 a)) = (a v b')
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud3lem1d  569
  Copyright terms: Public domain W3C validator