Theorem wdwom 1106

Description: Prove 2-variable WOML rule in WDOL. This will make all WOML theorems available to us. The proof does not use ax-r3 439 or ax-wom 361. Since this is the same as ax-wom 361, from here on we will freely use those theorems invoking ax-wom 361. (Contributed by NM, 4-Mar-2006.)

Hypothesis

Ref	Expression
wdwom.1	(a⊥ ∪ (a ∩ b)) = 1

Assertion

Ref	Expression
wdwom	(b ∪ (a⊥ ∩ b⊥ )) = 1

Proof of Theorem wdwom

Step	Hyp	Ref	Expression
1		df-i2 45	. . 3 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
2	1	ax-r1 35	. 2 (b ∪ (a⊥ ∩ b⊥ )) = (a →2 b)
3		le1 146	. . 3 (a →2 b) ≤ 1
4		df-i5 48	. . . . . 6 (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
5		df-i1 44	. . . . . . . . 9 (a →1 b) = (a⊥ ∪ (a ∩ b))
6		wdwom.1	. . . . . . . . 9 (a⊥ ∪ (a ∩ b)) = 1
7	5, 6	ax-r2 36	. . . . . . . 8 (a →1 b) = 1
8	7	wql1lem 287	. . . . . . 7 (a⊥ ∪ b) = 1
9		or4 84	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b)⊥ ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∪ b)⊥ ) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
10		anor1 88	. . . . . . . . . . . . 13 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
11	10	ax-r1 35	. . . . . . . . . . . 12 (a⊥ ∪ b)⊥ = (a ∩ b⊥ )
12	11	lor 70	. . . . . . . . . . 11 ((a ∩ b) ∪ (a⊥ ∪ b)⊥ ) = ((a ∩ b) ∪ (a ∩ b⊥ ))
13	12	ax-r5 38	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∪ b)⊥ ) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
14	9, 13	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b)⊥ ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
15		or12 80	. . . . . . . . 9 ((a⊥ ∪ b)⊥ ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b)⊥ ∪ (a⊥ ∩ b⊥ )))
16		df-cmtr 134	. . . . . . . . 9 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
17	14, 15, 16	3tr1 63	. . . . . . . 8 ((a⊥ ∪ b)⊥ ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))) = C (a, b)
18		wdcom 1105	. . . . . . . 8 C (a, b) = 1
19	17, 18	ax-r2 36	. . . . . . 7 ((a⊥ ∪ b)⊥ ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))) = 1
20	8, 19	skr0 242	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) = 1
21	4, 20	ax-r2 36	. . . . 5 (a →5 b) = 1
22	21	ax-r1 35	. . . 4 1 = (a →5 b)
23		i5lei2 348	. . . 4 (a →5 b) ≤ (a →2 b)
24	22, 23	bltr 138	. . 3 1 ≤ (a →2 b)
25	3, 24	lebi 145	. 2 (a →2 b) = 1
26	2, 25	ax-r2 36	1 (b ∪ (a⊥ ∩ b⊥ )) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12   →₂ wi2 13   →₅ wi5 16   C wcmtr 29

This proof depends on 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-wdol 1104

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-i5 48  df-le1 130  df-le2 131  df-cmtr 134

This theorem is used by: (None)