QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  vneulemexp GIF version
Theorem vneulemexp 1148
Description: Expanded version of vneulem 1147. (Contributed by NM, 31-Mar-2011.)
Hypothesis
Ref Expression
vneulemexp.1 ((a ∪ b) ∩ (c ∪ d)) = 0
Assertion
Ref Expression
vneulemexp ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Proof of Theorem vneulemexp
StepHypRef Expression
1 ax-a2 31 . . . . . . 7 (a ∪ b) = (b ∪ a)
21ax-r5 38 . . . . . 6 ((a ∪ b) ∪ c) = ((b ∪ a) ∪ c)
3 or32 82 . . . . . 6 ((a ∪ c) ∪ d) = ((a ∪ d) ∪ c)
42, 32an 79 . . . . 5 (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) = (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c))
5 orcom 73 . . . . . . . . . . . 12 (b ∪ a) = (a ∪ b)
65ror 71 . . . . . . . . . . 11 ((b ∪ a) ∪ c) = ((a ∪ b) ∪ c)
7 or32 82 . . . . . . . . . . 11 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ b)
86, 7tr 62 . . . . . . . . . 10 ((b ∪ a) ∪ c) = ((a ∪ c) ∪ b)
9 or32 82 . . . . . . . . . 10 ((a ∪ d) ∪ c) = ((a ∪ c) ∪ d)
108, 92an 79 . . . . . . . . 9 (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c)) = (((a ∪ c) ∪ b) ∩ ((a ∪ c) ∪ d))
11 ancom 74 . . . . . . . . . 10 (((a ∪ c) ∪ b) ∩ ((a ∪ c) ∪ d)) = (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b))
12 ml 1123 . . . . . . . . . . 11 ((a ∪ c) ∪ (d ∩ ((a ∪ c) ∪ b))) = (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b))
1312cm 61 . . . . . . . . . 10 (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b)) = ((a ∪ c) ∪ (d ∩ ((a ∪ c) ∪ b)))
14 ancom 74 . . . . . . . . . . 11 (d ∩ ((a ∪ c) ∪ b)) = (((a ∪ c) ∪ b) ∩ d)
1514lor 70 . . . . . . . . . 10 ((a ∪ c) ∪ (d ∩ ((a ∪ c) ∪ b))) = ((a ∪ c) ∪ (((a ∪ c) ∪ b) ∩ d))
1611, 13, 153tr 65 . . . . . . . . 9 (((a ∪ c) ∪ b) ∩ ((a ∪ c) ∪ d)) = ((a ∪ c) ∪ (((a ∪ c) ∪ b) ∩ d))
1710, 16ax-r2 36 . . . . . . . 8 (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c)) = ((a ∪ c) ∪ (((a ∪ c) ∪ b) ∩ d))
18 leor 159 . . . . . . . . 9 (a ∪ c) ≤ ((d ∩ b) ∪ (a ∪ c))
19 or32 82 . . . . . . . . . . . 12 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ c)
2019ran 78 . . . . . . . . . . 11 (((a ∪ c) ∪ b) ∩ d) = (((a ∪ b) ∪ c) ∩ d)
21 leor 159 . . . . . . . . . . . . . . 15 d ≤ (c ∪ d)
22 leid 148 . . . . . . . . . . . . . . 15 d ≤ d
2321, 22ler2an 173 . . . . . . . . . . . . . 14 d ≤ ((c ∪ d) ∩ d)
24 lear 161 . . . . . . . . . . . . . 14 ((c ∪ d) ∩ d) ≤ d
2523, 24lebi 145 . . . . . . . . . . . . 13 d = ((c ∪ d) ∩ d)
2625lan 77 . . . . . . . . . . . 12 (((a ∪ b) ∪ c) ∩ d) = (((a ∪ b) ∪ c) ∩ ((c ∪ d) ∩ d))
27 anass 76 . . . . . . . . . . . . . 14 ((((a ∪ b) ∪ c) ∩ (c ∪ d)) ∩ d) = (((a ∪ b) ∪ c) ∩ ((c ∪ d) ∩ d))
2827cm 61 . . . . . . . . . . . . 13 (((a ∪ b) ∪ c) ∩ ((c ∪ d) ∩ d)) = ((((a ∪ b) ∪ c) ∩ (c ∪ d)) ∩ d)
29 ax-a2 31 . . . . . . . . . . . . . . . 16 ((a ∪ b) ∪ c) = (c ∪ (a ∪ b))
3029ran 78 . . . . . . . . . . . . . . 15 (((a ∪ b) ∪ c) ∩ (c ∪ d)) = ((c ∪ (a ∪ b)) ∩ (c ∪ d))
31 ml 1123 . . . . . . . . . . . . . . . 16 (c ∪ ((a ∪ b) ∩ (c ∪ d))) = ((c ∪ (a ∪ b)) ∩ (c ∪ d))
3231cm 61 . . . . . . . . . . . . . . 15 ((c ∪ (a ∪ b)) ∩ (c ∪ d)) = (c ∪ ((a ∪ b) ∩ (c ∪ d)))
33 orcom 73 . . . . . . . . . . . . . . 15 (c ∪ ((a ∪ b) ∩ (c ∪ d))) = (((a ∪ b) ∩ (c ∪ d)) ∪ c)
3430, 32, 333tr 65 . . . . . . . . . . . . . 14 (((a ∪ b) ∪ c) ∩ (c ∪ d)) = (((a ∪ b) ∩ (c ∪ d)) ∪ c)
3534ran 78 . . . . . . . . . . . . 13 ((((a ∪ b) ∪ c) ∩ (c ∪ d)) ∩ d) = ((((a ∪ b) ∩ (c ∪ d)) ∪ c) ∩ d)
3628, 35tr 62 . . . . . . . . . . . 12 (((a ∪ b) ∪ c) ∩ ((c ∪ d) ∩ d)) = ((((a ∪ b) ∩ (c ∪ d)) ∪ c) ∩ d)
37 vneulemexp.1 . . . . . . . . . . . . . . 15 ((a ∪ b) ∩ (c ∪ d)) = 0
3837ror 71 . . . . . . . . . . . . . 14 (((a ∪ b) ∩ (c ∪ d)) ∪ c) = (0 ∪ c)
39 or0r 103 . . . . . . . . . . . . . 14 (0 ∪ c) = c
4038, 39tr 62 . . . . . . . . . . . . 13 (((a ∪ b) ∩ (c ∪ d)) ∪ c) = c
4140ran 78 . . . . . . . . . . . 12 ((((a ∪ b) ∩ (c ∪ d)) ∪ c) ∩ d) = (c ∩ d)
4226, 36, 413tr 65 . . . . . . . . . . 11 (((a ∪ b) ∪ c) ∩ d) = (c ∩ d)
4320, 42tr 62 . . . . . . . . . 10 (((a ∪ c) ∪ b) ∩ d) = (c ∩ d)
44 leao3 164 . . . . . . . . . . 11 (c ∩ d) ≤ (a ∪ c)
4544lerr 150 . . . . . . . . . 10 (c ∩ d) ≤ ((d ∩ b) ∪ (a ∪ c))
4643, 45bltr 138 . . . . . . . . 9 (((a ∪ c) ∪ b) ∩ d) ≤ ((d ∩ b) ∪ (a ∪ c))
4718, 46lel2or 170 . . . . . . . 8 ((a ∪ c) ∪ (((a ∪ c) ∪ b) ∩ d)) ≤ ((d ∩ b) ∪ (a ∪ c))
4817, 47bltr 138 . . . . . . 7 (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c)) ≤ ((d ∩ b) ∪ (a ∪ c))
49 leao2 163 . . . . . . . . . 10 (d ∩ b) ≤ (b ∪ a)
5049ler 149 . . . . . . . . 9 (d ∩ b) ≤ ((b ∪ a) ∪ c)
51 leor 159 . . . . . . . . . 10 a ≤ (b ∪ a)
5251leror 152 . . . . . . . . 9 (a ∪ c) ≤ ((b ∪ a) ∪ c)
5350, 52lel2or 170 . . . . . . . 8 ((d ∩ b) ∪ (a ∪ c)) ≤ ((b ∪ a) ∪ c)
54 leao3 164 . . . . . . . . . 10 (d ∩ b) ≤ (a ∪ d)
5554ler 149 . . . . . . . . 9 (d ∩ b) ≤ ((a ∪ d) ∪ c)
56 leo 158 . . . . . . . . . 10 a ≤ (a ∪ d)
5756leror 152 . . . . . . . . 9 (a ∪ c) ≤ ((a ∪ d) ∪ c)
5855, 57lel2or 170 . . . . . . . 8 ((d ∩ b) ∪ (a ∪ c)) ≤ ((a ∪ d) ∪ c)
5953, 58ler2an 173 . . . . . . 7 ((d ∩ b) ∪ (a ∪ c)) ≤ (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c))
6048, 59lebi 145 . . . . . 6 (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c)) = ((d ∩ b) ∪ (a ∪ c))
61 leao1 162 . . . . . . . . . . 11 (d ∩ b) ≤ (d ∪ c)
6249, 61ler2an 173 . . . . . . . . . 10 (d ∩ b) ≤ ((b ∪ a) ∩ (d ∪ c))
63 orcom 73 . . . . . . . . . . . 12 (d ∪ c) = (c ∪ d)
645, 632an 79 . . . . . . . . . . 11 ((b ∪ a) ∩ (d ∪ c)) = ((a ∪ b) ∩ (c ∪ d))
6564, 37tr 62 . . . . . . . . . 10 ((b ∪ a) ∩ (d ∪ c)) = 0
6662, 65lbtr 139 . . . . . . . . 9 (d ∩ b) ≤ 0
67 le0 147 . . . . . . . . 9 0 ≤ (d ∩ b)
6866, 67lebi 145 . . . . . . . 8 (d ∩ b) = 0
6968ror 71 . . . . . . 7 ((d ∩ b) ∪ (a ∪ c)) = (0 ∪ (a ∪ c))
70 or0r 103 . . . . . . 7 (0 ∪ (a ∪ c)) = (a ∪ c)
7169, 70tr 62 . . . . . 6 ((d ∩ b) ∪ (a ∪ c)) = (a ∪ c)
7260, 71tr 62 . . . . 5 (((b ∪ a) ∪ c) ∩ ((a ∪ d) ∪ c)) = (a ∪ c)
734, 72tr 62 . . . 4 (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) = (a ∪ c)
74 orcom 73 . . . . . . . . . . 11 (a ∪ b) = (b ∪ a)
7574ror 71 . . . . . . . . . 10 ((a ∪ b) ∪ d) = ((b ∪ a) ∪ d)
76 or32 82 . . . . . . . . . 10 ((b ∪ a) ∪ d) = ((b ∪ d) ∪ a)
7775, 76tr 62 . . . . . . . . 9 ((a ∪ b) ∪ d) = ((b ∪ d) ∪ a)
78 or32 82 . . . . . . . . 9 ((b ∪ c) ∪ d) = ((b ∪ d) ∪ c)
7977, 782an 79 . . . . . . . 8 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = (((b ∪ d) ∪ a) ∩ ((b ∪ d) ∪ c))
80 ancom 74 . . . . . . . . 9 (((b ∪ d) ∪ a) ∩ ((b ∪ d) ∪ c)) = (((b ∪ d) ∪ c) ∩ ((b ∪ d) ∪ a))
81 ml 1123 . . . . . . . . . 10 ((b ∪ d) ∪ (c ∩ ((b ∪ d) ∪ a))) = (((b ∪ d) ∪ c) ∩ ((b ∪ d) ∪ a))
8281cm 61 . . . . . . . . 9 (((b ∪ d) ∪ c) ∩ ((b ∪ d) ∪ a)) = ((b ∪ d) ∪ (c ∩ ((b ∪ d) ∪ a)))
83 ancom 74 . . . . . . . . . 10 (c ∩ ((b ∪ d) ∪ a)) = (((b ∪ d) ∪ a) ∩ c)
8483lor 70 . . . . . . . . 9 ((b ∪ d) ∪ (c ∩ ((b ∪ d) ∪ a))) = ((b ∪ d) ∪ (((b ∪ d) ∪ a) ∩ c))
8580, 82, 843tr 65 . . . . . . . 8 (((b ∪ d) ∪ a) ∩ ((b ∪ d) ∪ c)) = ((b ∪ d) ∪ (((b ∪ d) ∪ a) ∩ c))
8679, 85ax-r2 36 . . . . . . 7 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = ((b ∪ d) ∪ (((b ∪ d) ∪ a) ∩ c))
87 leor 159 . . . . . . . 8 (b ∪ d) ≤ ((c ∩ a) ∪ (b ∪ d))
88 or32 82 . . . . . . . . . . 11 ((b ∪ d) ∪ a) = ((b ∪ a) ∪ d)
8988ran 78 . . . . . . . . . 10 (((b ∪ d) ∪ a) ∩ c) = (((b ∪ a) ∪ d) ∩ c)
90 leor 159 . . . . . . . . . . . . . 14 c ≤ (d ∪ c)
91 leid 148 . . . . . . . . . . . . . 14 c ≤ c
9290, 91ler2an 173 . . . . . . . . . . . . 13 c ≤ ((d ∪ c) ∩ c)
93 lear 161 . . . . . . . . . . . . 13 ((d ∪ c) ∩ c) ≤ c
9492, 93lebi 145 . . . . . . . . . . . 12 c = ((d ∪ c) ∩ c)
9594lan 77 . . . . . . . . . . 11 (((b ∪ a) ∪ d) ∩ c) = (((b ∪ a) ∪ d) ∩ ((d ∪ c) ∩ c))
96 anass 76 . . . . . . . . . . . . 13 ((((b ∪ a) ∪ d) ∩ (d ∪ c)) ∩ c) = (((b ∪ a) ∪ d) ∩ ((d ∪ c) ∩ c))
9796cm 61 . . . . . . . . . . . 12 (((b ∪ a) ∪ d) ∩ ((d ∪ c) ∩ c)) = ((((b ∪ a) ∪ d) ∩ (d ∪ c)) ∩ c)
98 ax-a2 31 . . . . . . . . . . . . . . 15 ((b ∪ a) ∪ d) = (d ∪ (b ∪ a))
9998ran 78 . . . . . . . . . . . . . 14 (((b ∪ a) ∪ d) ∩ (d ∪ c)) = ((d ∪ (b ∪ a)) ∩ (d ∪ c))
100 ml 1123 . . . . . . . . . . . . . . 15 (d ∪ ((b ∪ a) ∩ (d ∪ c))) = ((d ∪ (b ∪ a)) ∩ (d ∪ c))
101100cm 61 . . . . . . . . . . . . . 14 ((d ∪ (b ∪ a)) ∩ (d ∪ c)) = (d ∪ ((b ∪ a) ∩ (d ∪ c)))
102 orcom 73 . . . . . . . . . . . . . 14 (d ∪ ((b ∪ a) ∩ (d ∪ c))) = (((b ∪ a) ∩ (d ∪ c)) ∪ d)
10399, 101, 1023tr 65 . . . . . . . . . . . . 13 (((b ∪ a) ∪ d) ∩ (d ∪ c)) = (((b ∪ a) ∩ (d ∪ c)) ∪ d)
104103ran 78 . . . . . . . . . . . 12 ((((b ∪ a) ∪ d) ∩ (d ∪ c)) ∩ c) = ((((b ∪ a) ∩ (d ∪ c)) ∪ d) ∩ c)
10597, 104tr 62 . . . . . . . . . . 11 (((b ∪ a) ∪ d) ∩ ((d ∪ c) ∩ c)) = ((((b ∪ a) ∩ (d ∪ c)) ∪ d) ∩ c)
10665ror 71 . . . . . . . . . . . . 13 (((b ∪ a) ∩ (d ∪ c)) ∪ d) = (0 ∪ d)
107 or0r 103 . . . . . . . . . . . . 13 (0 ∪ d) = d
108106, 107tr 62 . . . . . . . . . . . 12 (((b ∪ a) ∩ (d ∪ c)) ∪ d) = d
109108ran 78 . . . . . . . . . . 11 ((((b ∪ a) ∩ (d ∪ c)) ∪ d) ∩ c) = (d ∩ c)
11095, 105, 1093tr 65 . . . . . . . . . 10 (((b ∪ a) ∪ d) ∩ c) = (d ∩ c)
11189, 110tr 62 . . . . . . . . 9 (((b ∪ d) ∪ a) ∩ c) = (d ∩ c)
112 leao3 164 . . . . . . . . . 10 (d ∩ c) ≤ (b ∪ d)
113112lerr 150 . . . . . . . . 9 (d ∩ c) ≤ ((c ∩ a) ∪ (b ∪ d))
114111, 113bltr 138 . . . . . . . 8 (((b ∪ d) ∪ a) ∩ c) ≤ ((c ∩ a) ∪ (b ∪ d))
11587, 114lel2or 170 . . . . . . 7 ((b ∪ d) ∪ (((b ∪ d) ∪ a) ∩ c)) ≤ ((c ∩ a) ∪ (b ∪ d))
11686, 115bltr 138 . . . . . 6 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) ≤ ((c ∩ a) ∪ (b ∪ d))
117 leao2 163 . . . . . . . . 9 (c ∩ a) ≤ (a ∪ b)
118117ler 149 . . . . . . . 8 (c ∩ a) ≤ ((a ∪ b) ∪ d)
119 leor 159 . . . . . . . . 9 b ≤ (a ∪ b)
120119leror 152 . . . . . . . 8 (b ∪ d) ≤ ((a ∪ b) ∪ d)
121118, 120lel2or 170 . . . . . . 7 ((c ∩ a) ∪ (b ∪ d)) ≤ ((a ∪ b) ∪ d)
122 leao3 164 . . . . . . . . 9 (c ∩ a) ≤ (b ∪ c)
123122ler 149 . . . . . . . 8 (c ∩ a) ≤ ((b ∪ c) ∪ d)
124 leo 158 . . . . . . . . 9 b ≤ (b ∪ c)
125124leror 152 . . . . . . . 8 (b ∪ d) ≤ ((b ∪ c) ∪ d)
126123, 125lel2or 170 . . . . . . 7 ((c ∩ a) ∪ (b ∪ d)) ≤ ((b ∪ c) ∪ d)
127121, 126ler2an 173 . . . . . 6 ((c ∩ a) ∪ (b ∪ d)) ≤ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))
128116, 127lebi 145 . . . . 5 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = ((c ∩ a) ∪ (b ∪ d))
129 leao1 162 . . . . . . . . . 10 (c ∩ a) ≤ (c ∪ d)
130117, 129ler2an 173 . . . . . . . . 9 (c ∩ a) ≤ ((a ∪ b) ∩ (c ∪ d))
131130, 37lbtr 139 . . . . . . . 8 (c ∩ a) ≤ 0
132 le0 147 . . . . . . . 8 0 ≤ (c ∩ a)
133131, 132lebi 145 . . . . . . 7 (c ∩ a) = 0
134133ror 71 . . . . . 6 ((c ∩ a) ∪ (b ∪ d)) = (0 ∪ (b ∪ d))
135 or0r 103 . . . . . 6 (0 ∪ (b ∪ d)) = (b ∪ d)
136134, 135tr 62 . . . . 5 ((c ∩ a) ∪ (b ∪ d)) = (b ∪ d)
137128, 136tr 62 . . . 4 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = (b ∪ d)
13873, 1372an 79 . . 3 ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((a ∪ c) ∩ (b ∪ d))
139138cm 61 . 2 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)))
140 ancom 74 . . 3 ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)))
141 an4 86 . . . 4 ((((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d))) = ((((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) ∩ (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)))
142 ancom 74 . . . . . . 7 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))
143 ancom 74 . . . . . . . 8 (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) = (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c))
144 ml 1123 . . . . . . . . 9 ((a ∪ b) ∪ (d ∩ ((a ∪ b) ∪ c))) = (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c))
145144cm 61 . . . . . . . 8 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = ((a ∪ b) ∪ (d ∩ ((a ∪ b) ∪ c)))
146 ancom 74 . . . . . . . . 9 (d ∩ ((a ∪ b) ∪ c)) = (((a ∪ b) ∪ c) ∩ d)
147146lor 70 . . . . . . . 8 ((a ∪ b) ∪ (d ∩ ((a ∪ b) ∪ c))) = ((a ∪ b) ∪ (((a ∪ b) ∪ c) ∩ d))
148143, 145, 1473tr 65 . . . . . . 7 (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) = ((a ∪ b) ∪ (((a ∪ b) ∪ c) ∩ d))
149142, 148ax-r2 36 . . . . . 6 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = ((a ∪ b) ∪ (((a ∪ b) ∪ c) ∩ d))
150 orcom 73 . . . . . 6 ((a ∪ b) ∪ (((a ∪ b) ∪ c) ∩ d)) = ((((a ∪ b) ∪ c) ∩ d) ∪ (a ∪ b))
15142ror 71 . . . . . 6 ((((a ∪ b) ∪ c) ∩ d) ∪ (a ∪ b)) = ((c ∩ d) ∪ (a ∪ b))
152149, 150, 1513tr 65 . . . . 5 (((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) = ((c ∩ d) ∪ (a ∪ b))
153 ax-a3 32 . . . . . . . 8 ((b ∪ c) ∪ d) = (b ∪ (c ∪ d))
154 orcom 73 . . . . . . . 8 (b ∪ (c ∪ d)) = ((c ∪ d) ∪ b)
155153, 154tr 62 . . . . . . 7 ((b ∪ c) ∪ d) = ((c ∪ d) ∪ b)
156 ax-a2 31 . . . . . . . . 9 (a ∪ c) = (c ∪ a)
157156ror 71 . . . . . . . 8 ((a ∪ c) ∪ d) = ((c ∪ a) ∪ d)
158 or32 82 . . . . . . . 8 ((c ∪ a) ∪ d) = ((c ∪ d) ∪ a)
159157, 158tr 62 . . . . . . 7 ((a ∪ c) ∪ d) = ((c ∪ d) ∪ a)
160155, 1592an 79 . . . . . 6 (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a))
161 ancom 74 . . . . . . . 8 (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a)) = (((c ∪ d) ∪ a) ∩ ((c ∪ d) ∪ b))
162 ancom 74 . . . . . . . . 9 (((c ∪ d) ∪ a) ∩ ((c ∪ d) ∪ b)) = (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a))
163 ml 1123 . . . . . . . . . 10 ((c ∪ d) ∪ (b ∩ ((c ∪ d) ∪ a))) = (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a))
164163cm 61 . . . . . . . . 9 (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a)) = ((c ∪ d) ∪ (b ∩ ((c ∪ d) ∪ a)))
165 ancom 74 . . . . . . . . . 10 (b ∩ ((c ∪ d) ∪ a)) = (((c ∪ d) ∪ a) ∩ b)
166165lor 70 . . . . . . . . 9 ((c ∪ d) ∪ (b ∩ ((c ∪ d) ∪ a))) = ((c ∪ d) ∪ (((c ∪ d) ∪ a) ∩ b))
167162, 164, 1663tr 65 . . . . . . . 8 (((c ∪ d) ∪ a) ∩ ((c ∪ d) ∪ b)) = ((c ∪ d) ∪ (((c ∪ d) ∪ a) ∩ b))
168161, 167ax-r2 36 . . . . . . 7 (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a)) = ((c ∪ d) ∪ (((c ∪ d) ∪ a) ∩ b))
169 orcom 73 . . . . . . 7 ((c ∪ d) ∪ (((c ∪ d) ∪ a) ∩ b)) = ((((c ∪ d) ∪ a) ∩ b) ∪ (c ∪ d))
170 leid 148 . . . . . . . . . . . 12 b ≤ b
171119, 170ler2an 173 . . . . . . . . . . 11 b ≤ ((a ∪ b) ∩ b)
172 lear 161 . . . . . . . . . . 11 ((a ∪ b) ∩ b) ≤ b
173171, 172lebi 145 . . . . . . . . . 10 b = ((a ∪ b) ∩ b)
174173lan 77 . . . . . . . . 9 (((c ∪ d) ∪ a) ∩ b) = (((c ∪ d) ∪ a) ∩ ((a ∪ b) ∩ b))
175 anass 76 . . . . . . . . . . 11 ((((c ∪ d) ∪ a) ∩ (a ∪ b)) ∩ b) = (((c ∪ d) ∪ a) ∩ ((a ∪ b) ∩ b))
176175cm 61 . . . . . . . . . 10 (((c ∪ d) ∪ a) ∩ ((a ∪ b) ∩ b)) = ((((c ∪ d) ∪ a) ∩ (a ∪ b)) ∩ b)
177 ax-a2 31 . . . . . . . . . . . . 13 ((c ∪ d) ∪ a) = (a ∪ (c ∪ d))
178177ran 78 . . . . . . . . . . . 12 (((c ∪ d) ∪ a) ∩ (a ∪ b)) = ((a ∪ (c ∪ d)) ∩ (a ∪ b))
179 ml 1123 . . . . . . . . . . . . 13 (a ∪ ((c ∪ d) ∩ (a ∪ b))) = ((a ∪ (c ∪ d)) ∩ (a ∪ b))
180179cm 61 . . . . . . . . . . . 12 ((a ∪ (c ∪ d)) ∩ (a ∪ b)) = (a ∪ ((c ∪ d) ∩ (a ∪ b)))
181 orcom 73 . . . . . . . . . . . 12 (a ∪ ((c ∪ d) ∩ (a ∪ b))) = (((c ∪ d) ∩ (a ∪ b)) ∪ a)
182178, 180, 1813tr 65 . . . . . . . . . . 11 (((c ∪ d) ∪ a) ∩ (a ∪ b)) = (((c ∪ d) ∩ (a ∪ b)) ∪ a)
183182ran 78 . . . . . . . . . 10 ((((c ∪ d) ∪ a) ∩ (a ∪ b)) ∩ b) = ((((c ∪ d) ∩ (a ∪ b)) ∪ a) ∩ b)
184176, 183tr 62 . . . . . . . . 9 (((c ∪ d) ∪ a) ∩ ((a ∪ b) ∩ b)) = ((((c ∪ d) ∩ (a ∪ b)) ∪ a) ∩ b)
185 ancom 74 . . . . . . . . . . . . 13 ((c ∪ d) ∩ (a ∪ b)) = ((a ∪ b) ∩ (c ∪ d))
186185, 37tr 62 . . . . . . . . . . . 12 ((c ∪ d) ∩ (a ∪ b)) = 0
187186ror 71 . . . . . . . . . . 11 (((c ∪ d) ∩ (a ∪ b)) ∪ a) = (0 ∪ a)
188 or0r 103 . . . . . . . . . . 11 (0 ∪ a) = a
189187, 188tr 62 . . . . . . . . . 10 (((c ∪ d) ∩ (a ∪ b)) ∪ a) = a
190189ran 78 . . . . . . . . 9 ((((c ∪ d) ∩ (a ∪ b)) ∪ a) ∩ b) = (a ∩ b)
191174, 184, 1903tr 65 . . . . . . . 8 (((c ∪ d) ∪ a) ∩ b) = (a ∩ b)
192191ror 71 . . . . . . 7 ((((c ∪ d) ∪ a) ∩ b) ∪ (c ∪ d)) = ((a ∩ b) ∪ (c ∪ d))
193168, 169, 1923tr 65 . . . . . 6 (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a)) = ((a ∩ b) ∪ (c ∪ d))
194 orcom 73 . . . . . 6 ((a ∩ b) ∪ (c ∪ d)) = ((c ∪ d) ∪ (a ∩ b))
195160, 193, 1943tr 65 . . . . 5 (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = ((c ∪ d) ∪ (a ∩ b))
196152, 1952an 79 . . . 4 ((((a ∪ b) ∪ d) ∩ ((a ∪ b) ∪ c)) ∩ (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d))) = (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b)))
197141, 196tr 62 . . 3 ((((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d))) = (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b)))
198 ml 1123 . . . . . . 7 ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b))))) = (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b))))
199198cm 61 . . . . . 6 (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b)))) = ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b)))))
200 orass 75 . . . . . . . . 9 (((c ∩ d) ∪ (c ∪ d)) ∪ (a ∩ b)) = ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b)))
201200cm 61 . . . . . . . 8 ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b))) = (((c ∩ d) ∪ (c ∪ d)) ∪ (a ∩ b))
202 leao1 162 . . . . . . . . . 10 (c ∩ d) ≤ (c ∪ d)
203202df-le2 131 . . . . . . . . 9 ((c ∩ d) ∪ (c ∪ d)) = (c ∪ d)
204203ror 71 . . . . . . . 8 (((c ∩ d) ∪ (c ∪ d)) ∪ (a ∩ b)) = ((c ∪ d) ∪ (a ∩ b))
205201, 204tr 62 . . . . . . 7 ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b))) = ((c ∪ d) ∪ (a ∩ b))
206205lan 77 . . . . . 6 (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b)))) = (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b)))
207205lan 77 . . . . . . 7 ((a ∪ b) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b)))) = ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b)))
208207lor 70 . . . . . 6 ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∩ d) ∪ ((c ∪ d) ∪ (a ∩ b))))) = ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))))
209199, 206, 2083tr2 64 . . . . 5 (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))))
210 leao1 162 . . . . . . . . . . 11 (a ∩ b) ≤ (a ∪ b)
211 leid 148 . . . . . . . . . . 11 (a ∩ b) ≤ (a ∩ b)
212210, 211ler2an 173 . . . . . . . . . 10 (a ∩ b) ≤ ((a ∪ b) ∩ (a ∩ b))
213 lear 161 . . . . . . . . . 10 ((a ∪ b) ∩ (a ∩ b)) ≤ (a ∩ b)
214212, 213lebi 145 . . . . . . . . 9 (a ∩ b) = ((a ∪ b) ∩ (a ∩ b))
215214lor 70 . . . . . . . 8 ((c ∪ d) ∪ (a ∩ b)) = ((c ∪ d) ∪ ((a ∪ b) ∩ (a ∩ b)))
216215lan 77 . . . . . . 7 ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((a ∪ b) ∩ ((c ∪ d) ∪ ((a ∪ b) ∩ (a ∩ b))))
217 mldual 1124 . . . . . . 7 ((a ∪ b) ∩ ((c ∪ d) ∪ ((a ∪ b) ∩ (a ∩ b)))) = (((a ∪ b) ∩ (c ∪ d)) ∪ ((a ∪ b) ∩ (a ∩ b)))
218213, 212lebi 145 . . . . . . . . 9 ((a ∪ b) ∩ (a ∩ b)) = (a ∩ b)
21937, 2182or 72 . . . . . . . 8 (((a ∪ b) ∩ (c ∪ d)) ∪ ((a ∪ b) ∩ (a ∩ b))) = (0 ∪ (a ∩ b))
220 or0r 103 . . . . . . . 8 (0 ∪ (a ∩ b)) = (a ∩ b)
221219, 220tr 62 . . . . . . 7 (((a ∪ b) ∩ (c ∪ d)) ∪ ((a ∪ b) ∩ (a ∩ b))) = (a ∩ b)
222216, 217, 2213tr 65 . . . . . 6 ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b))) = (a ∩ b)
223222lor 70 . . . . 5 ((c ∩ d) ∪ ((a ∪ b) ∩ ((c ∪ d) ∪ (a ∩ b)))) = ((c ∩ d) ∪ (a ∩ b))
224209, 223tr 62 . . . 4 (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((c ∩ d) ∪ (a ∩ b))
225 orcom 73 . . . 4 ((c ∩ d) ∪ (a ∩ b)) = ((a ∩ b) ∪ (c ∩ d))
226224, 225tr 62 . . 3 (((c ∩ d) ∪ (a ∪ b)) ∩ ((c ∪ d) ∪ (a ∩ b))) = ((a ∩ b) ∪ (c ∩ d))
227140, 197, 2263tr 65 . 2 ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((a ∩ b) ∪ (c ∩ d))
228139, 227tr 62 1 ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Colors of variables: term
Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7  0wf 9
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  ax-ml 1122
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator