Theorem i3bi 496

Description: Kalmbach implication and biconditional. (Contributed by NM, 5-Nov-1997.)

Assertion

Ref	Expression
i3bi	((a →3 b) ∩ (b →3 a)) = (a ≡ b)

Proof of Theorem i3bi

Step	Hyp	Ref	Expression
1		anor2 89	. . . . . . 7 (b⊥ ∩ a) = (b ∪ a⊥ )⊥
2		lea 160	. . . . . . . . . . . . 13 (a⊥ ∩ b) ≤ a⊥
3		leo 158	. . . . . . . . . . . . . 14 a⊥ ≤ (a⊥ ∪ b)
4		ax-a2 31	. . . . . . . . . . . . . 14 (a⊥ ∪ b) = (b ∪ a⊥ )
5	3, 4	lbtr 139	. . . . . . . . . . . . 13 a⊥ ≤ (b ∪ a⊥ )
6	2, 5	letr 137	. . . . . . . . . . . 12 (a⊥ ∩ b) ≤ (b ∪ a⊥ )
7		lea 160	. . . . . . . . . . . . 13 ((a⊥ ∪ b) ∩ a) ≤ (a⊥ ∪ b)
8		ancom 74	. . . . . . . . . . . . 13 (a ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b) ∩ a)
9		ax-a2 31	. . . . . . . . . . . . 13 (b ∪ a⊥ ) = (a⊥ ∪ b)
10	7, 8, 9	le3tr1 140	. . . . . . . . . . . 12 (a ∩ (a⊥ ∪ b)) ≤ (b ∪ a⊥ )
11	6, 10	le2or 168	. . . . . . . . . . 11 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ≤ ((b ∪ a⊥ ) ∪ (b ∪ a⊥ ))
12		oridm 110	. . . . . . . . . . 11 ((b ∪ a⊥ ) ∪ (b ∪ a⊥ )) = (b ∪ a⊥ )
13	11, 12	lbtr 139	. . . . . . . . . 10 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ≤ (b ∪ a⊥ )
14	13	lecom 180	. . . . . . . . 9 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) C (b ∪ a⊥ )
15	14	comcom2 183	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) C (b ∪ a⊥ )⊥
16	15	comcom 453	. . . . . . 7 (b ∪ a⊥ )⊥ C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
17	1, 16	bctr 181	. . . . . 6 (b⊥ ∩ a) C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
18		lea 160	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ a)) ≤ b
19		leo 158	. . . . . . . . . . 11 b ≤ (b ∪ a⊥ )
20	18, 19	letr 137	. . . . . . . . . 10 (b ∩ (b⊥ ∪ a)) ≤ (b ∪ a⊥ )
21	20	lecom 180	. . . . . . . . 9 (b ∩ (b⊥ ∪ a)) C (b ∪ a⊥ )
22	21	comcom2 183	. . . . . . . 8 (b ∩ (b⊥ ∪ a)) C (b ∪ a⊥ )⊥
23	22	comcom 453	. . . . . . 7 (b ∪ a⊥ )⊥ C (b ∩ (b⊥ ∪ a))
24	1, 23	bctr 181	. . . . . 6 (b⊥ ∩ a) C (b ∩ (b⊥ ∪ a))
25	17, 24	fh2 470	. . . . 5 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))) = ((((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b⊥ ∩ a)) ∪ (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b ∩ (b⊥ ∪ a))))
26		ancom 74	. . . . . . . 8 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
27		lea 160	. . . . . . . . . . . . . 14 (b⊥ ∩ a) ≤ b⊥
28		leo 158	. . . . . . . . . . . . . 14 b⊥ ≤ (b⊥ ∪ a)
29	27, 28	letr 137	. . . . . . . . . . . . 13 (b⊥ ∩ a) ≤ (b⊥ ∪ a)
30	29	lecom 180	. . . . . . . . . . . 12 (b⊥ ∩ a) C (b⊥ ∪ a)
31	30	comcom2 183	. . . . . . . . . . 11 (b⊥ ∩ a) C (b⊥ ∪ a)⊥
32		ancom 74	. . . . . . . . . . . . 13 (a⊥ ∩ b) = (b ∩ a⊥ )
33		anor1 88	. . . . . . . . . . . . 13 (b ∩ a⊥ ) = (b⊥ ∪ a)⊥
34	32, 33	ax-r2 36	. . . . . . . . . . . 12 (a⊥ ∩ b) = (b⊥ ∪ a)⊥
35	34	ax-r1 35	. . . . . . . . . . 11 (b⊥ ∪ a)⊥ = (a⊥ ∩ b)
36	31, 35	cbtr 182	. . . . . . . . . 10 (b⊥ ∩ a) C (a⊥ ∩ b)
37		ancom 74	. . . . . . . . . . . 12 (b⊥ ∩ a) = (a ∩ b⊥ )
38		anor1 88	. . . . . . . . . . . 12 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
39	37, 38	ax-r2 36	. . . . . . . . . . 11 (b⊥ ∩ a) = (a⊥ ∪ b)⊥
40	8, 7	bltr 138	. . . . . . . . . . . . . 14 (a ∩ (a⊥ ∪ b)) ≤ (a⊥ ∪ b)
41	40	lecom 180	. . . . . . . . . . . . 13 (a ∩ (a⊥ ∪ b)) C (a⊥ ∪ b)
42	41	comcom2 183	. . . . . . . . . . . 12 (a ∩ (a⊥ ∪ b)) C (a⊥ ∪ b)⊥
43	42	comcom 453	. . . . . . . . . . 11 (a⊥ ∪ b)⊥ C (a ∩ (a⊥ ∪ b))
44	39, 43	bctr 181	. . . . . . . . . 10 (b⊥ ∩ a) C (a ∩ (a⊥ ∪ b))
45	36, 44	fh1 469	. . . . . . . . 9 ((b⊥ ∩ a) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (((b⊥ ∩ a) ∩ (a⊥ ∩ b)) ∪ ((b⊥ ∩ a) ∩ (a ∩ (a⊥ ∪ b))))
46	37	ran 78	. . . . . . . . . . . 12 ((b⊥ ∩ a) ∩ (a⊥ ∩ b)) = ((a ∩ b⊥ ) ∩ (a⊥ ∩ b))
47		an4 86	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∩ (a⊥ ∩ b)) = ((a ∩ a⊥ ) ∩ (b⊥ ∩ b))
48		dff 101	. . . . . . . . . . . . . . . 16 0 = (a ∩ a⊥ )
49		dff 101	. . . . . . . . . . . . . . . . 17 0 = (b ∩ b⊥ )
50		ancom 74	. . . . . . . . . . . . . . . . 17 (b ∩ b⊥ ) = (b⊥ ∩ b)
51	49, 50	ax-r2 36	. . . . . . . . . . . . . . . 16 0 = (b⊥ ∩ b)
52	48, 51	2an 79	. . . . . . . . . . . . . . 15 (0 ∩ 0) = ((a ∩ a⊥ ) ∩ (b⊥ ∩ b))
53	52	ax-r1 35	. . . . . . . . . . . . . 14 ((a ∩ a⊥ ) ∩ (b⊥ ∩ b)) = (0 ∩ 0)
54		anidm 111	. . . . . . . . . . . . . 14 (0 ∩ 0) = 0
55	53, 54	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ a⊥ ) ∩ (b⊥ ∩ b)) = 0
56	47, 55	ax-r2 36	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∩ (a⊥ ∩ b)) = 0
57	46, 56	ax-r2 36	. . . . . . . . . . 11 ((b⊥ ∩ a) ∩ (a⊥ ∩ b)) = 0
58		an12 81	. . . . . . . . . . . 12 ((b⊥ ∩ a) ∩ (a ∩ (a⊥ ∪ b))) = (a ∩ ((b⊥ ∩ a) ∩ (a⊥ ∪ b)))
59		dff 101	. . . . . . . . . . . . . . . 16 0 = ((b⊥ ∩ a) ∩ (b⊥ ∩ a)⊥ )
60	1	con2 67	. . . . . . . . . . . . . . . . . 18 (b⊥ ∩ a)⊥ = (b ∪ a⊥ )
61	60, 9	ax-r2 36	. . . . . . . . . . . . . . . . 17 (b⊥ ∩ a)⊥ = (a⊥ ∪ b)
62	61	lan 77	. . . . . . . . . . . . . . . 16 ((b⊥ ∩ a) ∩ (b⊥ ∩ a)⊥ ) = ((b⊥ ∩ a) ∩ (a⊥ ∪ b))
63	59, 62	ax-r2 36	. . . . . . . . . . . . . . 15 0 = ((b⊥ ∩ a) ∩ (a⊥ ∪ b))
64	63	lan 77	. . . . . . . . . . . . . 14 (a ∩ 0) = (a ∩ ((b⊥ ∩ a) ∩ (a⊥ ∪ b)))
65	64	ax-r1 35	. . . . . . . . . . . . 13 (a ∩ ((b⊥ ∩ a) ∩ (a⊥ ∪ b))) = (a ∩ 0)
66		an0 108	. . . . . . . . . . . . 13 (a ∩ 0) = 0
67	65, 66	ax-r2 36	. . . . . . . . . . . 12 (a ∩ ((b⊥ ∩ a) ∩ (a⊥ ∪ b))) = 0
68	58, 67	ax-r2 36	. . . . . . . . . . 11 ((b⊥ ∩ a) ∩ (a ∩ (a⊥ ∪ b))) = 0
69	57, 68	2or 72	. . . . . . . . . 10 (((b⊥ ∩ a) ∩ (a⊥ ∩ b)) ∪ ((b⊥ ∩ a) ∩ (a ∩ (a⊥ ∪ b)))) = (0 ∪ 0)
70		oridm 110	. . . . . . . . . 10 (0 ∪ 0) = 0
71	69, 70	ax-r2 36	. . . . . . . . 9 (((b⊥ ∩ a) ∩ (a⊥ ∩ b)) ∪ ((b⊥ ∩ a) ∩ (a ∩ (a⊥ ∪ b)))) = 0
72	45, 71	ax-r2 36	. . . . . . . 8 ((b⊥ ∩ a) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = 0
73	26, 72	ax-r2 36	. . . . . . 7 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b⊥ ∩ a)) = 0
74		ancom 74	. . . . . . . 8 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b ∩ (b⊥ ∪ a))) = ((b ∩ (b⊥ ∪ a)) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
75		ancom 74	. . . . . . . . . . . . . . 15 (b ∩ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∩ b)
76		lea 160	. . . . . . . . . . . . . . 15 ((b⊥ ∪ a) ∩ b) ≤ (b⊥ ∪ a)
77	75, 76	bltr 138	. . . . . . . . . . . . . 14 (b ∩ (b⊥ ∪ a)) ≤ (b⊥ ∪ a)
78	77	lecom 180	. . . . . . . . . . . . 13 (b ∩ (b⊥ ∪ a)) C (b⊥ ∪ a)
79	78	comcom2 183	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ a)) C (b⊥ ∪ a)⊥
80	79	comcom 453	. . . . . . . . . . 11 (b⊥ ∪ a)⊥ C (b ∩ (b⊥ ∪ a))
81	34, 80	bctr 181	. . . . . . . . . 10 (a⊥ ∩ b) C (b ∩ (b⊥ ∪ a))
82		anor2 89	. . . . . . . . . . 11 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
83		lea 160	. . . . . . . . . . . . . . 15 (a ∩ (a⊥ ∪ b)) ≤ a
84		leo 158	. . . . . . . . . . . . . . 15 a ≤ (a ∪ b⊥ )
85	83, 84	letr 137	. . . . . . . . . . . . . 14 (a ∩ (a⊥ ∪ b)) ≤ (a ∪ b⊥ )
86	85	lecom 180	. . . . . . . . . . . . 13 (a ∩ (a⊥ ∪ b)) C (a ∪ b⊥ )
87	86	comcom2 183	. . . . . . . . . . . 12 (a ∩ (a⊥ ∪ b)) C (a ∪ b⊥ )⊥
88	87	comcom 453	. . . . . . . . . . 11 (a ∪ b⊥ )⊥ C (a ∩ (a⊥ ∪ b))
89	82, 88	bctr 181	. . . . . . . . . 10 (a⊥ ∩ b) C (a ∩ (a⊥ ∪ b))
90	81, 89	fh2 470	. . . . . . . . 9 ((b ∩ (b⊥ ∪ a)) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))))
91		ax-a2 31	. . . . . . . . . 10 (((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b)))) = (((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)))
92		an4 86	. . . . . . . . . . . . 13 ((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))) = ((b ∩ a) ∩ ((b⊥ ∪ a) ∩ (a⊥ ∪ b)))
93		anandi 114	. . . . . . . . . . . . . 14 ((b ∩ a) ∩ ((b⊥ ∪ a) ∩ (a⊥ ∪ b))) = (((b ∩ a) ∩ (b⊥ ∪ a)) ∩ ((b ∩ a) ∩ (a⊥ ∪ b)))
94		coman1 185	. . . . . . . . . . . . . . . . . . 19 (b ∩ a) C b
95	94	comcom2 183	. . . . . . . . . . . . . . . . . 18 (b ∩ a) C b⊥
96		ancom 74	. . . . . . . . . . . . . . . . . . 19 (b ∩ a) = (a ∩ b)
97		coman1 185	. . . . . . . . . . . . . . . . . . 19 (a ∩ b) C a
98	96, 97	bctr 181	. . . . . . . . . . . . . . . . . 18 (b ∩ a) C a
99	95, 98	fh1 469	. . . . . . . . . . . . . . . . 17 ((b ∩ a) ∩ (b⊥ ∪ a)) = (((b ∩ a) ∩ b⊥ ) ∪ ((b ∩ a) ∩ a))
100		an32 83	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ a) ∩ b⊥ ) = ((b ∩ b⊥ ) ∩ a)
101		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 ((b ∩ b⊥ ) ∩ a) = (a ∩ (b ∩ b⊥ ))
102	49	lan 77	. . . . . . . . . . . . . . . . . . . . . . . 24 (a ∩ 0) = (a ∩ (b ∩ b⊥ ))
103	102	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . . 23 (a ∩ (b ∩ b⊥ )) = (a ∩ 0)
104	103, 66	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . 22 (a ∩ (b ∩ b⊥ )) = 0
105	101, 104	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ b⊥ ) ∩ a) = 0
106	100, 105	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b ∩ a) ∩ b⊥ ) = 0
107		anass 76	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ a) ∩ a) = (b ∩ (a ∩ a))
108		anidm 111	. . . . . . . . . . . . . . . . . . . . . 22 (a ∩ a) = a
109	108	lan 77	. . . . . . . . . . . . . . . . . . . . 21 (b ∩ (a ∩ a)) = (b ∩ a)
110	107, 109	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b ∩ a) ∩ a) = (b ∩ a)
111	106, 110	2or 72	. . . . . . . . . . . . . . . . . . 19 (((b ∩ a) ∩ b⊥ ) ∪ ((b ∩ a) ∩ a)) = (0 ∪ (b ∩ a))
112		ax-a2 31	. . . . . . . . . . . . . . . . . . 19 (0 ∪ (b ∩ a)) = ((b ∩ a) ∪ 0)
113	111, 112	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (((b ∩ a) ∩ b⊥ ) ∪ ((b ∩ a) ∩ a)) = ((b ∩ a) ∪ 0)
114		or0 102	. . . . . . . . . . . . . . . . . 18 ((b ∩ a) ∪ 0) = (b ∩ a)
115	113, 114	ax-r2 36	. . . . . . . . . . . . . . . . 17 (((b ∩ a) ∩ b⊥ ) ∪ ((b ∩ a) ∩ a)) = (b ∩ a)
116	99, 115	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b ∩ a) ∩ (b⊥ ∪ a)) = (b ∩ a)
117	98	comcom2 183	. . . . . . . . . . . . . . . . . 18 (b ∩ a) C a⊥
118	117, 94	fh1 469	. . . . . . . . . . . . . . . . 17 ((b ∩ a) ∩ (a⊥ ∪ b)) = (((b ∩ a) ∩ a⊥ ) ∪ ((b ∩ a) ∩ b))
119		anass 76	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ a) ∩ a⊥ ) = (b ∩ (a ∩ a⊥ ))
120	48	lan 77	. . . . . . . . . . . . . . . . . . . . . . 23 (b ∩ 0) = (b ∩ (a ∩ a⊥ ))
121	120	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . 22 (b ∩ (a ∩ a⊥ )) = (b ∩ 0)
122		an0 108	. . . . . . . . . . . . . . . . . . . . . 22 (b ∩ 0) = 0
123	121, 122	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 (b ∩ (a ∩ a⊥ )) = 0
124	119, 123	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b ∩ a) ∩ a⊥ ) = 0
125		an32 83	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ a) ∩ b) = ((b ∩ b) ∩ a)
126		anidm 111	. . . . . . . . . . . . . . . . . . . . . 22 (b ∩ b) = b
127	126	ran 78	. . . . . . . . . . . . . . . . . . . . 21 ((b ∩ b) ∩ a) = (b ∩ a)
128	125, 127	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b ∩ a) ∩ b) = (b ∩ a)
129	124, 128	2or 72	. . . . . . . . . . . . . . . . . . 19 (((b ∩ a) ∩ a⊥ ) ∪ ((b ∩ a) ∩ b)) = (0 ∪ (b ∩ a))
130	129, 112	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (((b ∩ a) ∩ a⊥ ) ∪ ((b ∩ a) ∩ b)) = ((b ∩ a) ∪ 0)
131	130, 114	ax-r2 36	. . . . . . . . . . . . . . . . 17 (((b ∩ a) ∩ a⊥ ) ∪ ((b ∩ a) ∩ b)) = (b ∩ a)
132	118, 131	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b ∩ a) ∩ (a⊥ ∪ b)) = (b ∩ a)
133	116, 132	2an 79	. . . . . . . . . . . . . . 15 (((b ∩ a) ∩ (b⊥ ∪ a)) ∩ ((b ∩ a) ∩ (a⊥ ∪ b))) = ((b ∩ a) ∩ (b ∩ a))
134		anidm 111	. . . . . . . . . . . . . . . 16 ((b ∩ a) ∩ (b ∩ a)) = (b ∩ a)
135	134, 96	ax-r2 36	. . . . . . . . . . . . . . 15 ((b ∩ a) ∩ (b ∩ a)) = (a ∩ b)
136	133, 135	ax-r2 36	. . . . . . . . . . . . . 14 (((b ∩ a) ∩ (b⊥ ∪ a)) ∩ ((b ∩ a) ∩ (a⊥ ∪ b))) = (a ∩ b)
137	93, 136	ax-r2 36	. . . . . . . . . . . . 13 ((b ∩ a) ∩ ((b⊥ ∪ a) ∩ (a⊥ ∪ b))) = (a ∩ b)
138	92, 137	ax-r2 36	. . . . . . . . . . . 12 ((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))) = (a ∩ b)
139		anass 76	. . . . . . . . . . . . . 14 ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) = (b ∩ ((b⊥ ∪ a) ∩ (a⊥ ∩ b)))
140		dff 101	. . . . . . . . . . . . . . . . 17 0 = ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ )
141	35	lan 77	. . . . . . . . . . . . . . . . 17 ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ ) = ((b⊥ ∪ a) ∩ (a⊥ ∩ b))
142	140, 141	ax-r2 36	. . . . . . . . . . . . . . . 16 0 = ((b⊥ ∪ a) ∩ (a⊥ ∩ b))
143	142	lan 77	. . . . . . . . . . . . . . 15 (b ∩ 0) = (b ∩ ((b⊥ ∪ a) ∩ (a⊥ ∩ b)))
144	143	ax-r1 35	. . . . . . . . . . . . . 14 (b ∩ ((b⊥ ∪ a) ∩ (a⊥ ∩ b))) = (b ∩ 0)
145	139, 144	ax-r2 36	. . . . . . . . . . . . 13 ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) = (b ∩ 0)
146	145, 122	ax-r2 36	. . . . . . . . . . . 12 ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) = 0
147	138, 146	2or 72	. . . . . . . . . . 11 (((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b))) = ((a ∩ b) ∪ 0)
148		or0 102	. . . . . . . . . . 11 ((a ∩ b) ∪ 0) = (a ∩ b)
149	147, 148	ax-r2 36	. . . . . . . . . 10 (((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b))) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b))) = (a ∩ b)
150	91, 149	ax-r2 36	. . . . . . . . 9 (((b ∩ (b⊥ ∪ a)) ∩ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∪ a)) ∩ (a ∩ (a⊥ ∪ b)))) = (a ∩ b)
151	90, 150	ax-r2 36	. . . . . . . 8 ((b ∩ (b⊥ ∪ a)) ∩ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (a ∩ b)
152	74, 151	ax-r2 36	. . . . . . 7 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b ∩ (b⊥ ∪ a))) = (a ∩ b)
153	73, 152	2or 72	. . . . . 6 ((((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b⊥ ∩ a)) ∪ (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b ∩ (b⊥ ∪ a)))) = (0 ∪ (a ∩ b))
154		ax-a2 31	. . . . . . 7 (0 ∪ (a ∩ b)) = ((a ∩ b) ∪ 0)
155	154, 148	ax-r2 36	. . . . . 6 (0 ∪ (a ∩ b)) = (a ∩ b)
156	153, 155	ax-r2 36	. . . . 5 ((((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b⊥ ∩ a)) ∪ (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ (b ∩ (b⊥ ∪ a)))) = (a ∩ b)
157	25, 156	ax-r2 36	. . . 4 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))) = (a ∩ b)
158	157	lor 70	. . 3 ((a⊥ ∩ b⊥ ) ∪ (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ b))
159		ancom 74	. . . . . 6 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
160		oran 87	. . . . . . . 8 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
161	160	ax-r1 35	. . . . . . 7 (b⊥ ∩ a⊥ )⊥ = (b ∪ a)
162	161	con3 68	. . . . . 6 (b⊥ ∩ a⊥ ) = (b ∪ a)⊥
163	159, 162	ax-r2 36	. . . . 5 (a⊥ ∩ b⊥ ) = (b ∪ a)⊥
164		lea 160	. . . . . . . . . 10 (b ∩ a⊥ ) ≤ b
165	32, 164	bltr 138	. . . . . . . . 9 (a⊥ ∩ b) ≤ b
166	165, 83	le2or 168	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ≤ (b ∪ a)
167	166	lecom 180	. . . . . . 7 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) C (b ∪ a)
168	167	comcom2 183	. . . . . 6 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) C (b ∪ a)⊥
169	168	comcom 453	. . . . 5 (b ∪ a)⊥ C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
170	163, 169	bctr 181	. . . 4 (a⊥ ∩ b⊥ ) C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
171		oran 87	. . . . . . 7 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
172	171	ax-r1 35	. . . . . 6 (a⊥ ∩ b⊥ )⊥ = (a ∪ b)
173	172	con3 68	. . . . 5 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
174		lea 160	. . . . . . . . . 10 (a ∩ b⊥ ) ≤ a
175	37, 174	bltr 138	. . . . . . . . 9 (b⊥ ∩ a) ≤ a
176	175, 18	le2or 168	. . . . . . . 8 ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ≤ (a ∪ b)
177	176	lecom 180	. . . . . . 7 ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) C (a ∪ b)
178	177	comcom2 183	. . . . . 6 ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) C (a ∪ b)⊥
179	178	comcom 453	. . . . 5 (a ∪ b)⊥ C ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))
180	173, 179	bctr 181	. . . 4 (a⊥ ∩ b⊥ ) C ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))
181	170, 180	fh3 471	. . 3 ((a⊥ ∩ b⊥ ) ∪ (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∩ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))) = (((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))))
182		ax-a2 31	. . 3 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
183	158, 181, 182	3tr2 64	. 2 (((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
184		df-i3 46	. . . 4 (a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))
185		or32 82	. . . . 5 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∪ (a⊥ ∩ b⊥ ))
186		ax-a2 31	. . . . 5 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
187	185, 186	ax-r2 36	. . . 4 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = ((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
188	184, 187	ax-r2 36	. . 3 (a →3 b) = ((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
189		df-i3 46	. . . 4 (b →3 a) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))
190		or32 82	. . . . 5 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))) = (((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ∪ (b⊥ ∩ a⊥ ))
191		ancom 74	. . . . . . 7 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
192	191	lor 70	. . . . . 6 (((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ∪ (b⊥ ∩ a⊥ )) = (((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ∪ (a⊥ ∩ b⊥ ))
193		ax-a2 31	. . . . . 6 (((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))
194	192, 193	ax-r2 36	. . . . 5 (((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))) ∪ (b⊥ ∩ a⊥ )) = ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))
195	190, 194	ax-r2 36	. . . 4 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))) = ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))
196	189, 195	ax-r2 36	. . 3 (b →3 a) = ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a))))
197	188, 196	2an 79	. 2 ((a →3 b) ∩ (b →3 a)) = (((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∩ b⊥ ) ∪ ((b⊥ ∩ a) ∪ (b ∩ (b⊥ ∪ a)))))
198		dfb 94	. 2 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
199	183, 197, 198	3tr1 63	1 ((a →3 b) ∩ (b →3 a)) = (a ≡ b)

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  0wf 9   →₃ wi3 14

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  i3or  497  bii3  516  u3lembi  723