[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ud4lem1c 579
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud4lem1c ((a ->4 b)' v (b ->4 a)) = (a v b')
Proof of Theorem ud4lem1c
StepHypRef Expression
1 ud4lem0c 280 . . 3 (a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
2 df-i4 47 . . 3 (b ->4 a) = (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
31, 22or 72 . 2 ((a ->4 b)' v (b ->4 a)) = ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
4 comor2 462 . . . . . . . . . . . 12 (a' v b') C b'
54comcom3 454 . . . . . . . . . . 11 (a' v b')' C b'
65comcom5 458 . . . . . . . . . 10 (a' v b') C b
7 comor1 461 . . . . . . . . . . . 12 (a' v b') C a'
87comcom3 454 . . . . . . . . . . 11 (a' v b')' C a'
98comcom5 458 . . . . . . . . . 10 (a' v b') C a
106, 9com2an 484 . . . . . . . . 9 (a' v b') C (b ^ a)
114, 9com2an 484 . . . . . . . . 9 (a' v b') C (b' ^ a)
1210, 11com2or 483 . . . . . . . 8 (a' v b') C ((b ^ a) v (b' ^ a))
1312comcom 453 . . . . . . 7 ((b ^ a) v (b' ^ a)) C (a' v b')
14 comor2 462 . . . . . . . . . . . 12 (a v b') C b'
1514comcom3 454 . . . . . . . . . . 11 (a v b')' C b'
1615comcom5 458 . . . . . . . . . 10 (a v b') C b
17 comor1 461 . . . . . . . . . 10 (a v b') C a
1816, 17com2an 484 . . . . . . . . 9 (a v b') C (b ^ a)
1914, 17com2an 484 . . . . . . . . 9 (a v b') C (b' ^ a)
2018, 19com2or 483 . . . . . . . 8 (a v b') C ((b ^ a) v (b' ^ a))
2120comcom 453 . . . . . . 7 ((b ^ a) v (b' ^ a)) C (a v b')
2213, 21com2an 484 . . . . . 6 ((b ^ a) v (b' ^ a)) C ((a' v b') ^ (a v b'))
2322comcom 453 . . . . 5 ((a' v b') ^ (a v b')) C ((b ^ a) v (b' ^ a))
24 comor2 462 . . . . . . . . . 10 (b' v a) C a
2524comcom2 183 . . . . . . . . 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')
2825comcom3 454 . . . . . . . . . 10 (b' v a)' C a'
2928comcom5 458 . . . . . . . . 9 (b' v a) C a
3029, 26com2or 483 . . . . . . . 8 (b' v a) C (a v b')
3127, 30com2an 484 . . . . . . 7 (b' v a) C ((a' v b') ^ (a v b'))
3231comcom 453 . . . . . 6 ((a' v b') ^ (a v b')) C (b' v a)
33 comorr 184 . . . . . . . 8 a' C (a' v b')
34 comorr 184 . . . . . . . . 9 a C (a v b')
3534comcom3 454 . . . . . . . 8 a' C (a v b')
3633, 35com2an 484 . . . . . . 7 a' C ((a' v b') ^ (a v b'))
3736comcom 453 . . . . . 6 ((a' v b') ^ (a v b')) C a'
3832, 37com2an 484 . . . . 5 ((a' v b') ^ (a v b')) C ((b' v a) ^ a')
3923, 38com2or 483 . . . 4 ((a' v b') ^ (a v b')) C (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
40 coman1 185 . . . . . . . . 9 (a ^ b') C a
4140comcom2 183 . . . . . . . 8 (a ^ b') C a'
42 coman2 186 . . . . . . . 8 (a ^ b') C b'
4341, 42com2or 483 . . . . . . 7 (a ^ b') C (a' v b')
4440, 42com2or 483 . . . . . . 7 (a ^ b') C (a v b')
4543, 44com2an 484 . . . . . 6 (a ^ b') C ((a' v b') ^ (a v b'))
4645comcom 453 . . . . 5 ((a' v b') ^ (a v b')) C (a ^ b')
474comcom 453 . . . . . . . . 9 b' C (a' v b')
4814comcom 453 . . . . . . . . 9 b' C (a v b')
4947, 48com2an 484 . . . . . . . 8 b' C ((a' v b') ^ (a v b'))
5049comcom 453 . . . . . . 7 ((a' v b') ^ (a v b')) C b'
5150comcom3 454 . . . . . 6 ((a' v b') ^ (a v b'))' C b'
5251comcom5 458 . . . . 5 ((a' v b') ^ (a v b')) C b
5346, 52com2or 483 . . . 4 ((a' v b') ^ (a v b')) C ((a ^ b') v b)
5439, 53fh4r 476 . . 3 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = ((((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))))
55 coman2 186 . . . . . . . . . . . 12 (b ^ a) C a
5655comcom2 183 . . . . . . . . . . 11 (b ^ a) C a'
57 coman1 185 . . . . . . . . . . . 12 (b ^ a) C b
5857comcom2 183 . . . . . . . . . . 11 (b ^ a) C b'
5956, 58com2or 483 . . . . . . . . . 10 (b ^ a) C (a' v b')
6059comcom 453 . . . . . . . . 9 (a' v b') C (b ^ a)
61 coman2 186 . . . . . . . . . . . 12 (b' ^ a) C a
6261comcom2 183 . . . . . . . . . . 11 (b' ^ a) C a'
63 coman1 185 . . . . . . . . . . 11 (b' ^ a) C b'
6462, 63com2or 483 . . . . . . . . . 10 (b' ^ a) C (a' v b')
6564comcom 453 . . . . . . . . 9 (a' v b') C (b' ^ a)
6660, 65com2or 483 . . . . . . . 8 (a' v b') C ((b ^ a) v (b' ^ a))
6727comcom 453 . . . . . . . . 9 (a' v b') C (b' v a)
6867, 7com2an 484 . . . . . . . 8 (a' v b') C ((b' v a) ^ a')
6966, 68com2or 483 . . . . . . 7 (a' v b') C (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
7017comcom2 183 . . . . . . . . 9 (a v b') C a'
7170, 14com2or 483 . . . . . . . 8 (a v b') C (a' v b')
7271comcom 453 . . . . . . 7 (a' v b') C (a v b')
7369, 72fh4r 476 . . . . . 6 (((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))))
74 ax-a2 31 . . . . . . . . . . 11 (((a' v b') v (b ^ a)) v (b' ^ a)) = ((b' ^ a) v ((a' v b') v (b ^ a)))
75 ax-a3 32 . . . . . . . . . . 11 (((a' v b') v (b ^ a)) v (b' ^ a)) = ((a' v b') v ((b ^ a) v (b' ^ a)))
76 ax-a2 31 . . . . . . . . . . . . . . 15 (a' v b') = (b' v a')
77 df-a 40 . . . . . . . . . . . . . . 15 (b ^ a) = (b' v a')'
7876, 772or 72 . . . . . . . . . . . . . 14 ((a' v b') v (b ^ a)) = ((b' v a') v (b' v a')')
79 df-t 41 . . . . . . . . . . . . . . 15 1 = ((b' v a') v (b' v a')')
8079ax-r1 35 . . . . . . . . . . . . . 14 ((b' v a') v (b' v a')') = 1
8178, 80ax-r2 36 . . . . . . . . . . . . 13 ((a' v b') v (b ^ a)) = 1
8281lor 70 . . . . . . . . . . . 12 ((b' ^ a) v ((a' v b') v (b ^ a))) = ((b' ^ a) v 1)
83 or1 104 . . . . . . . . . . . 12 ((b' ^ a) v 1) = 1
8482, 83ax-r2 36 . . . . . . . . . . 11 ((b' ^ a) v ((a' v b') v (b ^ a))) = 1
8574, 75, 843tr2 64 . . . . . . . . . 10 ((a' v b') v ((b ^ a) v (b' ^ a))) = 1
8685ax-r5 38 . . . . . . . . 9 (((a' v b') v ((b ^ a) v (b' ^ a))) v ((b' v a) ^ a')) = (1 v ((b' v a) ^ a'))
87 ax-a3 32 . . . . . . . . 9 (((a' v b') v ((b ^ a) v (b' ^ a))) v ((b' v a) ^ a')) = ((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
88 ax-a2 31 . . . . . . . . . 10 (1 v ((b' v a) ^ a')) = (((b' v a) ^ a') v 1)
89 or1 104 . . . . . . . . . 10 (((b' v a