Theorem vneulem11 1141

Description: Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96. (Contributed by NM, 31-Mar-2011.)

Hypothesis

Ref	Expression
vneulem6.1	((a ∪ b) ∩ (c ∪ d)) = 0

Assertion

Ref	Expression
vneulem11	(((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = ((c ∪ d) ∪ (a ∩ b))

Proof of Theorem vneulem11

Step	Hyp	Ref	Expression
1		ax-a3 32	. . . 4 ((b ∪ c) ∪ d) = (b ∪ (c ∪ d))
2		orcom 73	. . . 4 (b ∪ (c ∪ d)) = ((c ∪ d) ∪ b)
3	1, 2	tr 62	. . 3 ((b ∪ c) ∪ d) = ((c ∪ d) ∪ b)
4		ax-a2 31	. . . . 5 (a ∪ c) = (c ∪ a)
5	4	ror 71	. . . 4 ((a ∪ c) ∪ d) = ((c ∪ a) ∪ d)
6		or32 82	. . . 4 ((c ∪ a) ∪ d) = ((c ∪ d) ∪ a)
7	5, 6	tr 62	. . 3 ((a ∪ c) ∪ d) = ((c ∪ d) ∪ a)
8	3, 7	2an 79	. 2 (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a))
9		ancom 74	. . . 4 ((c ∪ d) ∩ (a ∪ b)) = ((a ∪ b) ∩ (c ∪ d))
10		vneulem6.1	. . . 4 ((a ∪ b) ∩ (c ∪ d)) = 0
11	9, 10	tr 62	. . 3 ((c ∪ d) ∩ (a ∪ b)) = 0
12	11	vneulem9 1139	. 2 (((c ∪ d) ∪ b) ∩ ((c ∪ d) ∪ a)) = ((a ∩ b) ∪ (c ∪ d))
13		orcom 73	. 2 ((a ∩ b) ∪ (c ∪ d)) = ((c ∪ d) ∪ (a ∩ b))
14	8, 12, 13	3tr 65	1 (((b ∪ c) ∪ d) ∩ ((a ∪ c) ∪ d)) = ((c ∪ d) ∪ (a ∩ b))

This proof depends on syntax axioms:   = wb 1   ∪ wo 6   ∩ wa 7  0wf 9

This proof depends on 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 proof depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  vneulem16  1146