Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem orbi 824

Description: Disjunction of biconditionals.

**Assertion**
Ref	Expression
orbi	((a ≡ c) ∪ (b ≡ c)) = (((a →₂c) ∪ (b →₂c)) ∩ ((c →₁a) ∪ (c →₁b)))

**Proof of Theorem orbi**
Step	Hyp	Ref	Expression
1		dfb 86	. . 3 (a ≡ c) = ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))
2		dfb 86	. . 3 (b ≡ c) = ((b ∩ c) ∪ (b^⊥ ∩ c^⊥ ))
3	1, 2	2or 67	. 2 ((a ≡ c) ∪ (b ≡ c)) = (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b ∩ c) ∪ (b^⊥ ∩ c^⊥ )))
4		ax-a2 30	. 2 (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b ∩ c) ∪ (b^⊥ ∩ c^⊥ ))) = (((b ∩ c) ∪ (b^⊥ ∩ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
5		ax-a3 31	. . 3 (((b ∩ c) ∪ (b^⊥ ∩ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = ((b ∩ c) ∪ ((b^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))))
6		ancom 68	. . . . . . . 8 (a ∩ c) = (c ∩ a)
7	6	lor 66	. . . . . . 7 ((b^⊥ ∩ c^⊥ ) ∪ (a ∩ c)) = ((b^⊥ ∩ c^⊥ ) ∪ (c ∩ a))
8		imp3 823	. . . . . . . 8 ((b →₂c) ∩ (c →₁a)) = ((b^⊥ ∩ c^⊥ ) ∪ (c ∩ a))
9	8	ax-r1 34	. . . . . . 7 ((b^⊥ ∩ c^⊥ ) ∪ (c ∩ a)) = ((b →₂c) ∩ (c →₁a))
10	7, 9	ax-r2 35	. . . . . 6 ((b^⊥ ∩ c^⊥ ) ∪ (a ∩ c)) = ((b →₂c) ∩ (c →₁a))
11	10	ax-r5 37	. . . . 5 (((b^⊥ ∩ c^⊥ ) ∪ (a ∩ c)) ∪ (a^⊥ ∩ c^⊥ )) = (((b →₂c) ∩ (c →₁a)) ∪ (a^⊥ ∩ c^⊥ ))
12		ax-a3 31	. . . . 5 (((b^⊥ ∩ c^⊥ ) ∪ (a ∩ c)) ∪ (a^⊥ ∩ c^⊥ )) = ((b^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
13		df-i1 43	. . . . . . . 8 (c →₁a) = (c^⊥ ∪ (c ∩ a))
14		lear 153	. . . . . . . . . . 11 (a^⊥ ∩ c^⊥ ) ≤ c^⊥
15		leo 150	. . . . . . . . . . 11 c^⊥ ≤ (c^⊥ ∪ (c ∩ a))
16	14, 15	letr 129	. . . . . . . . . 10 (a^⊥ ∩ c^⊥ ) ≤ (c^⊥ ∪ (c ∩ a))
17	16	lecom 172	. . . . . . . . 9 (a^⊥ ∩ c^⊥ ) C (c^⊥ ∪ (c ∩ a))
18	17	comcom 435	. . . . . . . 8 (c^⊥ ∪ (c ∩ a)) C (a^⊥ ∩ c^⊥ )
19	13, 18	bctr 173	. . . . . . 7 (c →₁a) C (a^⊥ ∩ c^⊥ )
20		comi12 689	. . . . . . 7 (c →₁a) C (b →₂c)
21	19, 20	fh4rc 464	. . . . . 6 (((b →₂c) ∩ (c →₁a)) ∪ (a^⊥ ∩ c^⊥ )) = (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ ((c →₁a) ∪ (a^⊥ ∩ c^⊥ )))
22	13	ax-r5 37	. . . . . . . 8 ((c →₁a) ∪ (a^⊥ ∩ c^⊥ )) = ((c^⊥ ∪ (c ∩ a)) ∪ (a^⊥ ∩ c^⊥ ))
23		ax-a2 30	. . . . . . . 8 ((c^⊥ ∪ (c ∩ a)) ∪ (a^⊥ ∩ c^⊥ )) = ((a^⊥ ∩ c^⊥ ) ∪ (c^⊥ ∪ (c ∩ a)))
24	16	df-le2 123	. . . . . . . 8 ((a^⊥ ∩ c^⊥ ) ∪ (c^⊥ ∪ (c ∩ a))) = (c^⊥ ∪ (c ∩ a))
25	22, 23, 24	3tr 62	. . . . . . 7 ((c →₁a) ∪ (a^⊥ ∩ c^⊥ )) = (c^⊥ ∪ (c ∩ a))
26	25	lan 70	. . . . . 6 (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ ((c →₁a) ∪ (a^⊥ ∩ c^⊥ ))) = (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a)))
27	21, 26	ax-r2 35	. . . . 5 (((b →₂c) ∩ (c →₁a)) ∪ (a^⊥ ∩ c^⊥ )) = (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a)))
28	11, 12, 27	3tr2 61	. . . 4 ((b^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a)))
29	28	lor 66	. . 3 ((b ∩ c) ∪ ((b^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))) = ((b ∩ c) ∪ (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a))))
30		df-i2 44	. . . . . . . 8 (b →₂c) = (c ∪ (b^⊥ ∩ c^⊥ ))
31	30	ax-r5 37	. . . . . . 7 ((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) = ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (a^⊥ ∩ c^⊥ ))
32		ax-a3 31	. . . . . . 7 ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (a^⊥ ∩ c^⊥ )) = (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
33	31, 32	ax-r2 35	. . . . . 6 ((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) = (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
34		lear 153	. . . . . . . . 9 (b ∩ c) ≤ c
35		leo 150	. . . . . . . . 9 c ≤ (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
36	34, 35	letr 129	. . . . . . . 8 (b ∩ c) ≤ (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
37	36	lecom 172	. . . . . . 7 (b ∩ c) C (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
38	37	comcom 435	. . . . . 6 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) C (b ∩ c)
39	33, 38	bctr 173	. . . . 5 ((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) C (b ∩ c)
40		lea 152	. . . . . . . . . . 11 (c ∩ (c ∩ a)^⊥ ) ≤ c
41	40, 35	letr 129	. . . . . . . . . 10 (c ∩ (c ∩ a)^⊥ ) ≤ (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
42	41	lecom 172	. . . . . . . . 9 (c ∩ (c ∩ a)^⊥ ) C (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )))
43	42	comcom 435	. . . . . . . 8 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) C (c ∩ (c ∩ a)^⊥ )
44		anor1 80	. . . . . . . 8 (c ∩ (c ∩ a)^⊥ ) = (c^⊥ ∪ (c ∩ a))^⊥
45	43, 44	cbtr 174	. . . . . . 7 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) C (c^⊥ ∪ (c ∩ a))^⊥
46	45	comcom7 442	. . . . . 6 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) C (c^⊥ ∪ (c ∩ a))
47	33, 46	bctr 173	. . . . 5 ((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) C (c^⊥ ∪ (c ∩ a))
48	39, 47	fh4 454	. . . 4 ((b ∩ c) ∪ (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a)))) = (((b ∩ c) ∪ ((b →₂c) ∪ (a^⊥ ∩ c^⊥ ))) ∩ ((b ∩ c) ∪ (c^⊥ ∪ (c ∩ a))))
49	30	lor 66	. . . . . . . 8 ((b ∩ c) ∪ (b →₂c)) = ((b ∩ c) ∪ (c ∪ (b^⊥ ∩ c^⊥ )))
50		leo 150	. . . . . . . . . 10 c ≤ (c ∪ (b^⊥ ∩ c^⊥ ))
51	34, 50	letr 129	. . . . . . . . 9 (b ∩ c) ≤ (c ∪ (b^⊥ ∩ c^⊥ ))
52	51	df-le2 123	. . . . . . . 8 ((b ∩ c) ∪ (c ∪ (b^⊥ ∩ c^⊥ ))) = (c ∪ (b^⊥ ∩ c^⊥ ))
53	49, 52	ax-r2 35	. . . . . . 7 ((b ∩ c) ∪ (b →₂c)) = (c ∪ (b^⊥ ∩ c^⊥ ))
54	53	ax-r5 37	. . . . . 6 (((b ∩ c) ∪ (b →₂c)) ∪ (a^⊥ ∩ c^⊥ )) = ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (a^⊥ ∩ c^⊥ ))
55		ax-a3 31	. . . . . 6 (((b ∩ c) ∪ (b →₂c)) ∪ (a^⊥ ∩ c^⊥ )) = ((b ∩ c) ∪ ((b →₂c) ∪ (a^⊥ ∩ c^⊥ )))
56		ax-a2 30	. . . . . . . 8 ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (c ∪ (a^⊥ ∩ c^⊥ ))) = ((c ∪ (a^⊥ ∩ c^⊥ )) ∪ (c ∪ (b^⊥ ∩ c^⊥ )))
57		orordi 104	. . . . . . . 8 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) = ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (c ∪ (a^⊥ ∩ c^⊥ )))
58		df-i2 44	. . . . . . . . 9 (a →₂c) = (c ∪ (a^⊥ ∩ c^⊥ ))
59	58, 30	2or 67	. . . . . . . 8 ((a →₂c) ∪ (b →₂c)) = ((c ∪ (a^⊥ ∩ c^⊥ )) ∪ (c ∪ (b^⊥ ∩ c^⊥ )))
60	56, 57, 59	3tr1 60	. . . . . . 7 (c ∪ ((b^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ ))) = ((a →₂c) ∪ (b →₂c))
61	32, 60	ax-r2 35	. . . . . 6 ((c ∪ (b^⊥ ∩ c^⊥ )) ∪ (a^⊥ ∩ c^⊥ )) = ((a →₂c) ∪ (b →₂c))
62	54, 55, 61	3tr2 61	. . . . 5 ((b ∩ c) ∪ ((b →₂c) ∪ (a^⊥ ∩ c^⊥ ))) = ((a →₂c) ∪ (b →₂c))
63		or12 73	. . . . . 6 ((b ∩ c) ∪ (c^⊥ ∪ (c ∩ a))) = (c^⊥ ∪ ((b ∩ c) ∪ (c ∩ a)))
64		ax-a2 30	. . . . . . 7 ((c^⊥ ∪ (b ∩ c)) ∪ (c^⊥ ∪ (c ∩ a))) = ((c^⊥ ∪ (c ∩ a)) ∪ (c^⊥ ∪ (b ∩ c)))
65		orordi 104	. . . . . . 7 (c^⊥ ∪ ((b ∩ c) ∪ (c ∩ a))) = ((c^⊥ ∪ (b ∩ c)) ∪ (c^⊥ ∪ (c ∩ a)))
66		df-i1 43	. . . . . . . . 9 (c →₁b) = (c^⊥ ∪ (c ∩ b))
67		ancom 68	. . . . . . . . . 10 (c ∩ b) = (b ∩ c)
68	67	lor 66	. . . . . . . . 9 (c^⊥ ∪ (c ∩ b)) = (c^⊥ ∪ (b ∩ c))
69	66, 68	ax-r2 35	. . . . . . . 8 (c →₁b) = (c^⊥ ∪ (b ∩ c))
70	13, 69	2or 67	. . . . . . 7 ((c →₁a) ∪ (c →₁b)) = ((c^⊥ ∪ (c ∩ a)) ∪ (c^⊥ ∪ (b ∩ c)))
71	64, 65, 70	3tr1 60	. . . . . 6 (c^⊥ ∪ ((b ∩ c) ∪ (c ∩ a))) = ((c →₁a) ∪ (c →₁b))
72	63, 71	ax-r2 35	. . . . 5 ((b ∩ c) ∪ (c^⊥ ∪ (c ∩ a))) = ((c →₁a) ∪ (c →₁b))
73	62, 72	2an 72	. . . 4 (((b ∩ c) ∪ ((b →₂c) ∪ (a^⊥ ∩ c^⊥ ))) ∩ ((b ∩ c) ∪ (c^⊥ ∪ (c ∩ a)))) = (((a →₂c) ∪ (b →₂c)) ∩ ((c →₁a) ∪ (c →₁b)))
74	48, 73	ax-r2 35	. . 3 ((b ∩ c) ∪ (((b →₂c) ∪ (a^⊥ ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ a)))) = (((a →₂c) ∪ (b →₂c)) ∩ ((c →₁a) ∪ (c →₁b)))
75	5, 29, 74	3tr 62	. 2 (((b ∩ c) ∪ (b^⊥ ∩ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = (((a →₂c) ∪ (b →₂c)) ∩ ((c →₁a) ∪ (c →₁b)))
76	3, 4, 75	3tr 62	1 ((a ≡ c) ∪ (b ≡ c)) = (((a →₂c) ∪ (b →₂c)) ∩ ((c →₁a) ∪ (c →₁b)))

Colors of variables: term

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

This theorem is referenced by: orbile 825

This theorem was proved from axioms: ax-a1 29 ax-a2 30 ax-a3 31 ax-a4 32 ax-a5 33 ax-r1 34 ax-r2 35 ax-r4 36 ax-r5 37 ax-r3 421

This theorem depends on definitions: df-b 38 df-a 39 df-t 40 df-f 41 df-i1 43 df-i2 44 df-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org