Theorem wr5-2v 366

Description: WOML derived from 2-variable axioms. (Contributed by NM, 11-Nov-1998.)

Hypothesis

Ref	Expression
wr5-2v.1	(a ≡ b) = 1

Assertion

Ref	Expression
wr5-2v	((a ∪ c) ≡ (b ∪ c)) = 1

Proof of Theorem wr5-2v

Step	Hyp	Ref	Expression
1		df-i2 45	. . 3 ((a ∪ c) →2 (b ∪ c)) = ((b ∪ c) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
2		df-i2 45	. . . . 5 (a →2 (b ∪ c)) = ((b ∪ c) ∪ (a⊥ ∩ (b ∪ c)⊥ ))
3	2	ax-r1 35	. . . 4 ((b ∪ c) ∪ (a⊥ ∩ (b ∪ c)⊥ )) = (a →2 (b ∪ c))
4		anandir 115	. . . . . 6 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
5		anass 76	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
6		anor3 90	. . . . . . . 8 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
7	6	lan 77	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) = (a⊥ ∩ (b ∪ c)⊥ )
8	5, 7	ax-r2 36	. . . . . 6 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b ∪ c)⊥ )
9		anor3 90	. . . . . . 7 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
10	9, 6	2an 79	. . . . . 6 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )
11	4, 8, 10	3tr2 64	. . . . 5 (a⊥ ∩ (b ∪ c)⊥ ) = ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )
12	11	lor 70	. . . 4 ((b ∪ c) ∪ (a⊥ ∩ (b ∪ c)⊥ )) = ((b ∪ c) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
13		df-i1 44	. . . . . 6 (a →1 (b ∪ c)) = (a⊥ ∪ (a ∩ (b ∪ c)))
14		wr5-2v.1	. . . . . . . . . . . . . 14 (a ≡ b) = 1
15		wlem1 243	. . . . . . . . . . . . . 14 ((a ≡ b)⊥ ∪ ((a →1 b) ∩ (b →1 a))) = 1
16	14, 15	skr0 242	. . . . . . . . . . . . 13 ((a →1 b) ∩ (b →1 a)) = 1
17	16	ax-r1 35	. . . . . . . . . . . 12 1 = ((a →1 b) ∩ (b →1 a))
18		lea 160	. . . . . . . . . . . 12 ((a →1 b) ∩ (b →1 a)) ≤ (a →1 b)
19	17, 18	bltr 138	. . . . . . . . . . 11 1 ≤ (a →1 b)
20		le1 146	. . . . . . . . . . 11 (a →1 b) ≤ 1
21	19, 20	lebi 145	. . . . . . . . . 10 1 = (a →1 b)
22		df-i1 44	. . . . . . . . . 10 (a →1 b) = (a⊥ ∪ (a ∩ b))
23	21, 22	ax-r2 36	. . . . . . . . 9 1 = (a⊥ ∪ (a ∩ b))
24		leo 158	. . . . . . . . . . 11 b ≤ (b ∪ c)
25	24	lelan 167	. . . . . . . . . 10 (a ∩ b) ≤ (a ∩ (b ∪ c))
26	25	lelor 166	. . . . . . . . 9 (a⊥ ∪ (a ∩ b)) ≤ (a⊥ ∪ (a ∩ (b ∪ c)))
27	23, 26	bltr 138	. . . . . . . 8 1 ≤ (a⊥ ∪ (a ∩ (b ∪ c)))
28		le1 146	. . . . . . . 8 (a⊥ ∪ (a ∩ (b ∪ c))) ≤ 1
29	27, 28	lebi 145	. . . . . . 7 1 = (a⊥ ∪ (a ∩ (b ∪ c)))
30	29	ax-r1 35	. . . . . 6 (a⊥ ∪ (a ∩ (b ∪ c))) = 1
31	13, 30	ax-r2 36	. . . . 5 (a →1 (b ∪ c)) = 1
32	31	2vwomr1a 363	. . . 4 (a →2 (b ∪ c)) = 1
33	3, 12, 32	3tr2 64	. . 3 ((b ∪ c) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )) = 1
34	1, 33	ax-r2 36	. 2 ((a ∪ c) →2 (b ∪ c)) = 1
35		df-i2 45	. . 3 ((b ∪ c) →2 (a ∪ c)) = ((a ∪ c) ∪ ((b ∪ c)⊥ ∩ (a ∪ c)⊥ ))
36		df-i2 45	. . . . 5 (b →2 (a ∪ c)) = ((a ∪ c) ∪ (b⊥ ∩ (a ∪ c)⊥ ))
37	36	ax-r1 35	. . . 4 ((a ∪ c) ∪ (b⊥ ∩ (a ∪ c)⊥ )) = (b →2 (a ∪ c))
38		anandir 115	. . . . . 6 ((b⊥ ∩ a⊥ ) ∩ c⊥ ) = ((b⊥ ∩ c⊥ ) ∩ (a⊥ ∩ c⊥ ))
39		anass 76	. . . . . . 7 ((b⊥ ∩ a⊥ ) ∩ c⊥ ) = (b⊥ ∩ (a⊥ ∩ c⊥ ))
40	9	lan 77	. . . . . . 7 (b⊥ ∩ (a⊥ ∩ c⊥ )) = (b⊥ ∩ (a ∪ c)⊥ )
41	39, 40	ax-r2 36	. . . . . 6 ((b⊥ ∩ a⊥ ) ∩ c⊥ ) = (b⊥ ∩ (a ∪ c)⊥ )
42	6, 9	2an 79	. . . . . 6 ((b⊥ ∩ c⊥ ) ∩ (a⊥ ∩ c⊥ )) = ((b ∪ c)⊥ ∩ (a ∪ c)⊥ )
43	38, 41, 42	3tr2 64	. . . . 5 (b⊥ ∩ (a ∪ c)⊥ ) = ((b ∪ c)⊥ ∩ (a ∪ c)⊥ )
44	43	lor 70	. . . 4 ((a ∪ c) ∪ (b⊥ ∩ (a ∪ c)⊥ )) = ((a ∪ c) ∪ ((b ∪ c)⊥ ∩ (a ∪ c)⊥ ))
45		df-i1 44	. . . . . 6 (b →1 (a ∪ c)) = (b⊥ ∪ (b ∩ (a ∪ c)))
46		lear 161	. . . . . . . . . . . 12 ((a →1 b) ∩ (b →1 a)) ≤ (b →1 a)
47	17, 46	bltr 138	. . . . . . . . . . 11 1 ≤ (b →1 a)
48		le1 146	. . . . . . . . . . 11 (b →1 a) ≤ 1
49	47, 48	lebi 145	. . . . . . . . . 10 1 = (b →1 a)
50		df-i1 44	. . . . . . . . . 10 (b →1 a) = (b⊥ ∪ (b ∩ a))
51	49, 50	ax-r2 36	. . . . . . . . 9 1 = (b⊥ ∪ (b ∩ a))
52		leo 158	. . . . . . . . . . 11 a ≤ (a ∪ c)
53	52	lelan 167	. . . . . . . . . 10 (b ∩ a) ≤ (b ∩ (a ∪ c))
54	53	lelor 166	. . . . . . . . 9 (b⊥ ∪ (b ∩ a)) ≤ (b⊥ ∪ (b ∩ (a ∪ c)))
55	51, 54	bltr 138	. . . . . . . 8 1 ≤ (b⊥ ∪ (b ∩ (a ∪ c)))
56		le1 146	. . . . . . . 8 (b⊥ ∪ (b ∩ (a ∪ c))) ≤ 1
57	55, 56	lebi 145	. . . . . . 7 1 = (b⊥ ∪ (b ∩ (a ∪ c)))
58	57	ax-r1 35	. . . . . 6 (b⊥ ∪ (b ∩ (a ∪ c))) = 1
59	45, 58	ax-r2 36	. . . . 5 (b →1 (a ∪ c)) = 1
60	59	2vwomr1a 363	. . . 4 (b →2 (a ∪ c)) = 1
61	37, 44, 60	3tr2 64	. . 3 ((a ∪ c) ∪ ((b ∪ c)⊥ ∩ (a ∪ c)⊥ )) = 1
62	35, 61	ax-r2 36	. 2 ((b ∪ c) →2 (a ∪ c)) = 1
63	34, 62	2vwomlem 365	1 ((a ∪ c) ≡ (b ∪ c)) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12   →₂ wi2 13

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-wom 361

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le1 130  df-le2 131

This theorem is referenced by:  wom3  367  wlor  368  wran  369  wr2  371  w2or  372  wler  391  wleror  393  wletr  396  wbltr  397  wbile  401  wlecom  409  wcomcom2  415  wfh2  424  wr5  431  ska2  432  woml6  436  woml7  437