Theorem orbi 842

Description: Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)

Assertion

Ref	Expression
orbi	((a ≡ c) ∪ (b ≡ c)) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))

Proof of Theorem orbi

Step	Hyp	Ref	Expression
1		dfb 94	. . 3 (a ≡ c) = ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))
2		dfb 94	. . 3 (b ≡ c) = ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))
3	1, 2	2or 72	. 2 ((a ≡ c) ∪ (b ≡ c)) = (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b ∩ c) ∪ (b⊥ ∩ c⊥ )))
4		ax-a2 31	. 2 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))) = (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
5		ax-a3 32	. . 3 (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = ((b ∩ c) ∪ ((b⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))))
6		ancom 74	. . . . . . . 8 (a ∩ c) = (c ∩ a)
7	6	lor 70	. . . . . . 7 ((b⊥ ∩ c⊥ ) ∪ (a ∩ c)) = ((b⊥ ∩ c⊥ ) ∪ (c ∩ a))
8		imp3 841	. . . . . . . 8 ((b →2 c) ∩ (c →1 a)) = ((b⊥ ∩ c⊥ ) ∪ (c ∩ a))
9	8	ax-r1 35	. . . . . . 7 ((b⊥ ∩ c⊥ ) ∪ (c ∩ a)) = ((b →2 c) ∩ (c →1 a))
10	7, 9	ax-r2 36	. . . . . 6 ((b⊥ ∩ c⊥ ) ∪ (a ∩ c)) = ((b →2 c) ∩ (c →1 a))
11	10	ax-r5 38	. . . . 5 (((b⊥ ∩ c⊥ ) ∪ (a ∩ c)) ∪ (a⊥ ∩ c⊥ )) = (((b →2 c) ∩ (c →1 a)) ∪ (a⊥ ∩ c⊥ ))
12		ax-a3 32	. . . . 5 (((b⊥ ∩ c⊥ ) ∪ (a ∩ c)) ∪ (a⊥ ∩ c⊥ )) = ((b⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
13		df-i1 44	. . . . . . . 8 (c →1 a) = (c⊥ ∪ (c ∩ a))
14		lear 161	. . . . . . . . . . 11 (a⊥ ∩ c⊥ ) ≤ c⊥
15		leo 158	. . . . . . . . . . 11 c⊥ ≤ (c⊥ ∪ (c ∩ a))
16	14, 15	letr 137	. . . . . . . . . 10 (a⊥ ∩ c⊥ ) ≤ (c⊥ ∪ (c ∩ a))
17	16	lecom 180	. . . . . . . . 9 (a⊥ ∩ c⊥ ) C (c⊥ ∪ (c ∩ a))
18	17	comcom 453	. . . . . . . 8 (c⊥ ∪ (c ∩ a)) C (a⊥ ∩ c⊥ )
19	13, 18	bctr 181	. . . . . . 7 (c →1 a) C (a⊥ ∩ c⊥ )
20		comi12 707	. . . . . . 7 (c →1 a) C (b →2 c)
21	19, 20	fh4rc 482	. . . . . 6 (((b →2 c) ∩ (c →1 a)) ∪ (a⊥ ∩ c⊥ )) = (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ ((c →1 a) ∪ (a⊥ ∩ c⊥ )))
22	13	ax-r5 38	. . . . . . . 8 ((c →1 a) ∪ (a⊥ ∩ c⊥ )) = ((c⊥ ∪ (c ∩ a)) ∪ (a⊥ ∩ c⊥ ))
23		ax-a2 31	. . . . . . . 8 ((c⊥ ∪ (c ∩ a)) ∪ (a⊥ ∩ c⊥ )) = ((a⊥ ∩ c⊥ ) ∪ (c⊥ ∪ (c ∩ a)))
24	16	df-le2 131	. . . . . . . 8 ((a⊥ ∩ c⊥ ) ∪ (c⊥ ∪ (c ∩ a))) = (c⊥ ∪ (c ∩ a))
25	22, 23, 24	3tr 65	. . . . . . 7 ((c →1 a) ∪ (a⊥ ∩ c⊥ )) = (c⊥ ∪ (c ∩ a))
26	25	lan 77	. . . . . 6 (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ ((c →1 a) ∪ (a⊥ ∩ c⊥ ))) = (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a)))
27	21, 26	ax-r2 36	. . . . 5 (((b →2 c) ∩ (c →1 a)) ∪ (a⊥ ∩ c⊥ )) = (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a)))
28	11, 12, 27	3tr2 64	. . . 4 ((b⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a)))
29	28	lor 70	. . 3 ((b ∩ c) ∪ ((b⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))) = ((b ∩ c) ∪ (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a))))
30		df-i2 45	. . . . . . . 8 (b →2 c) = (c ∪ (b⊥ ∩ c⊥ ))
31	30	ax-r5 38	. . . . . . 7 ((b →2 c) ∪ (a⊥ ∩ c⊥ )) = ((c ∪ (b⊥ ∩ c⊥ )) ∪ (a⊥ ∩ c⊥ ))
32		ax-a3 32	. . . . . . 7 ((c ∪ (b⊥ ∩ c⊥ )) ∪ (a⊥ ∩ c⊥ )) = (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
33	31, 32	ax-r2 36	. . . . . 6 ((b →2 c) ∪ (a⊥ ∩ c⊥ )) = (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
34		lear 161	. . . . . . . . 9 (b ∩ c) ≤ c
35		leo 158	. . . . . . . . 9 c ≤ (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
36	34, 35	letr 137	. . . . . . . 8 (b ∩ c) ≤ (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
37	36	lecom 180	. . . . . . 7 (b ∩ c) C (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
38	37	comcom 453	. . . . . 6 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) C (b ∩ c)
39	33, 38	bctr 181	. . . . 5 ((b →2 c) ∪ (a⊥ ∩ c⊥ )) C (b ∩ c)
40		lea 160	. . . . . . . . . . 11 (c ∩ (c ∩ a)⊥ ) ≤ c
41	40, 35	letr 137	. . . . . . . . . 10 (c ∩ (c ∩ a)⊥ ) ≤ (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
42	41	lecom 180	. . . . . . . . 9 (c ∩ (c ∩ a)⊥ ) C (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )))
43	42	comcom 453	. . . . . . . 8 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) C (c ∩ (c ∩ a)⊥ )
44		anor1 88	. . . . . . . 8 (c ∩ (c ∩ a)⊥ ) = (c⊥ ∪ (c ∩ a))⊥
45	43, 44	cbtr 182	. . . . . . 7 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) C (c⊥ ∪ (c ∩ a))⊥
46	45	comcom7 460	. . . . . 6 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) C (c⊥ ∪ (c ∩ a))
47	33, 46	bctr 181	. . . . 5 ((b →2 c) ∪ (a⊥ ∩ c⊥ )) C (c⊥ ∪ (c ∩ a))
48	39, 47	fh4 472	. . . 4 ((b ∩ c) ∪ (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a)))) = (((b ∩ c) ∪ ((b →2 c) ∪ (a⊥ ∩ c⊥ ))) ∩ ((b ∩ c) ∪ (c⊥ ∪ (c ∩ a))))
49	30	lor 70	. . . . . . . 8 ((b ∩ c) ∪ (b →2 c)) = ((b ∩ c) ∪ (c ∪ (b⊥ ∩ c⊥ )))
50		leo 158	. . . . . . . . . 10 c ≤ (c ∪ (b⊥ ∩ c⊥ ))
51	34, 50	letr 137	. . . . . . . . 9 (b ∩ c) ≤ (c ∪ (b⊥ ∩ c⊥ ))
52	51	df-le2 131	. . . . . . . 8 ((b ∩ c) ∪ (c ∪ (b⊥ ∩ c⊥ ))) = (c ∪ (b⊥ ∩ c⊥ ))
53	49, 52	ax-r2 36	. . . . . . 7 ((b ∩ c) ∪ (b →2 c)) = (c ∪ (b⊥ ∩ c⊥ ))
54	53	ax-r5 38	. . . . . 6 (((b ∩ c) ∪ (b →2 c)) ∪ (a⊥ ∩ c⊥ )) = ((c ∪ (b⊥ ∩ c⊥ )) ∪ (a⊥ ∩ c⊥ ))
55		ax-a3 32	. . . . . 6 (((b ∩ c) ∪ (b →2 c)) ∪ (a⊥ ∩ c⊥ )) = ((b ∩ c) ∪ ((b →2 c) ∪ (a⊥ ∩ c⊥ )))
56		ax-a2 31	. . . . . . . 8 ((c ∪ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))) = ((c ∪ (a⊥ ∩ c⊥ )) ∪ (c ∪ (b⊥ ∩ c⊥ )))
57		orordi 112	. . . . . . . 8 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) = ((c ∪ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))
58		df-i2 45	. . . . . . . . 9 (a →2 c) = (c ∪ (a⊥ ∩ c⊥ ))
59	58, 30	2or 72	. . . . . . . 8 ((a →2 c) ∪ (b →2 c)) = ((c ∪ (a⊥ ∩ c⊥ )) ∪ (c ∪ (b⊥ ∩ c⊥ )))
60	56, 57, 59	3tr1 63	. . . . . . 7 (c ∪ ((b⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ ))) = ((a →2 c) ∪ (b →2 c))
61	32, 60	ax-r2 36	. . . . . 6 ((c ∪ (b⊥ ∩ c⊥ )) ∪ (a⊥ ∩ c⊥ )) = ((a →2 c) ∪ (b →2 c))
62	54, 55, 61	3tr2 64	. . . . 5 ((b ∩ c) ∪ ((b →2 c) ∪ (a⊥ ∩ c⊥ ))) = ((a →2 c) ∪ (b →2 c))
63		or12 80	. . . . . 6 ((b ∩ c) ∪ (c⊥ ∪ (c ∩ a))) = (c⊥ ∪ ((b ∩ c) ∪ (c ∩ a)))
64		ax-a2 31	. . . . . . 7 ((c⊥ ∪ (b ∩ c)) ∪ (c⊥ ∪ (c ∩ a))) = ((c⊥ ∪ (c ∩ a)) ∪ (c⊥ ∪ (b ∩ c)))
65		orordi 112	. . . . . . 7 (c⊥ ∪ ((b ∩ c) ∪ (c ∩ a))) = ((c⊥ ∪ (b ∩ c)) ∪ (c⊥ ∪ (c ∩ a)))
66		df-i1 44	. . . . . . . . 9 (c →1 b) = (c⊥ ∪ (c ∩ b))
67		ancom 74	. . . . . . . . . 10 (c ∩ b) = (b ∩ c)
68	67	lor 70	. . . . . . . . 9 (c⊥ ∪ (c ∩ b)) = (c⊥ ∪ (b ∩ c))
69	66, 68	ax-r2 36	. . . . . . . 8 (c →1 b) = (c⊥ ∪ (b ∩ c))
70	13, 69	2or 72	. . . . . . 7 ((c →1 a) ∪ (c →1 b)) = ((c⊥ ∪ (c ∩ a)) ∪ (c⊥ ∪ (b ∩ c)))
71	64, 65, 70	3tr1 63	. . . . . 6 (c⊥ ∪ ((b ∩ c) ∪ (c ∩ a))) = ((c →1 a) ∪ (c →1 b))
72	63, 71	ax-r2 36	. . . . 5 ((b ∩ c) ∪ (c⊥ ∪ (c ∩ a))) = ((c →1 a) ∪ (c →1 b))
73	62, 72	2an 79	. . . 4 (((b ∩ c) ∪ ((b →2 c) ∪ (a⊥ ∩ c⊥ ))) ∩ ((b ∩ c) ∪ (c⊥ ∪ (c ∩ a)))) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
74	48, 73	ax-r2 36	. . 3 ((b ∩ c) ∪ (((b →2 c) ∪ (a⊥ ∩ c⊥ )) ∩ (c⊥ ∪ (c ∩ a)))) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
75	5, 29, 74	3tr 65	. 2 (((b ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
76	3, 4, 75	3tr 65	1 ((a ≡ c) ∪ (b ≡ c)) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7   →₁ wi1 12   →₂ wi2 13

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-r3 439

This proof 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  df-c1 132  df-c2 133

This theorem is used by:  orbile  843