Theorem u4lem5 764

Description: Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)

Assertion

Ref	Expression
u4lem5	(a →4 (a →4 b)) = ((a⊥ ∩ b⊥ ) ∪ b)

Proof of Theorem u4lem5

Step	Hyp	Ref	Expression
1		df-i4 47	. 2 (a →4 (a →4 b)) = (((a ∩ (a →4 b)) ∪ (a⊥ ∩ (a →4 b))) ∪ ((a⊥ ∪ (a →4 b)) ∩ (a →4 b)⊥ ))
2		ancom 74	. . . . . . 7 (a ∩ (a →4 b)) = ((a →4 b) ∩ a)
3		u4lemaa 603	. . . . . . 7 ((a →4 b) ∩ a) = (a ∩ b)
4	2, 3	ax-r2 36	. . . . . 6 (a ∩ (a →4 b)) = (a ∩ b)
5		ancom 74	. . . . . . 7 (a⊥ ∩ (a →4 b)) = ((a →4 b) ∩ a⊥ )
6		u4lemana 608	. . . . . . 7 ((a →4 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
7	5, 6	ax-r2 36	. . . . . 6 (a⊥ ∩ (a →4 b)) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
8	4, 7	2or 72	. . . . 5 ((a ∩ (a →4 b)) ∪ (a⊥ ∩ (a →4 b))) = ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
9		ax-a3 32	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) = ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
10	9	ax-r1 35	. . . . 5 ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
11	8, 10	ax-r2 36	. . . 4 ((a ∩ (a →4 b)) ∪ (a⊥ ∩ (a →4 b))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
12		ax-a2 31	. . . . . . 7 (a⊥ ∪ (a →4 b)) = ((a →4 b) ∪ a⊥ )
13		u4lemona 628	. . . . . . 7 ((a →4 b) ∪ a⊥ ) = (a⊥ ∪ b)
14	12, 13	ax-r2 36	. . . . . 6 (a⊥ ∪ (a →4 b)) = (a⊥ ∪ b)
15		ud4lem0c 280	. . . . . 6 (a →4 b)⊥ = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
16	14, 15	2an 79	. . . . 5 ((a⊥ ∪ (a →4 b)) ∩ (a →4 b)⊥ ) = ((a⊥ ∪ b) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)))
17		ancom 74	. . . . . 6 ((a⊥ ∪ b) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))) = ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (a⊥ ∪ b))
18		anass 76	. . . . . . 7 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (a⊥ ∪ b)) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ (a⊥ ∪ b)))
19		comor1 461	. . . . . . . . . . . . 13 (a⊥ ∪ b) C a⊥
20	19	comcom7 460	. . . . . . . . . . . 12 (a⊥ ∪ b) C a
21		comor2 462	. . . . . . . . . . . . 13 (a⊥ ∪ b) C b
22	21	comcom2 183	. . . . . . . . . . . 12 (a⊥ ∪ b) C b⊥
23	20, 22	com2an 484	. . . . . . . . . . 11 (a⊥ ∪ b) C (a ∩ b⊥ )
24	23, 21	fh1r 473	. . . . . . . . . 10 (((a ∩ b⊥ ) ∪ b) ∩ (a⊥ ∪ b)) = (((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) ∪ (b ∩ (a⊥ ∪ b)))
25		ax-a2 31	. . . . . . . . . . 11 (((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) ∪ (b ∩ (a⊥ ∪ b))) = ((b ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)))
26		leor 159	. . . . . . . . . . . . . 14 b ≤ (a⊥ ∪ b)
27	26	df2le2 136	. . . . . . . . . . . . 13 (b ∩ (a⊥ ∪ b)) = b
28		oran2 92	. . . . . . . . . . . . . . 15 (a⊥ ∪ b) = (a ∩ b⊥ )⊥
29	28	lan 77	. . . . . . . . . . . . . 14 ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) = ((a ∩ b⊥ ) ∩ (a ∩ b⊥ )⊥ )
30		dff 101	. . . . . . . . . . . . . . 15 0 = ((a ∩ b⊥ ) ∩ (a ∩ b⊥ )⊥ )
31	30	ax-r1 35	. . . . . . . . . . . . . 14 ((a ∩ b⊥ ) ∩ (a ∩ b⊥ )⊥ ) = 0
32	29, 31	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) = 0
33	27, 32	2or 72	. . . . . . . . . . . 12 ((b ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b))) = (b ∪ 0)
34		or0 102	. . . . . . . . . . . 12 (b ∪ 0) = b
35	33, 34	ax-r2 36	. . . . . . . . . . 11 ((b ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b))) = b
36	25, 35	ax-r2 36	. . . . . . . . . 10 (((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) ∪ (b ∩ (a⊥ ∪ b))) = b
37	24, 36	ax-r2 36	. . . . . . . . 9 (((a ∩ b⊥ ) ∪ b) ∩ (a⊥ ∪ b)) = b
38	37	lan 77	. . . . . . . 8 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ (a⊥ ∪ b))) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ b)
39		ancom 74	. . . . . . . 8 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ b) = (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))
40	38, 39	ax-r2 36	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ (a⊥ ∪ b))) = (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))
41	18, 40	ax-r2 36	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (a⊥ ∪ b)) = (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))
42	17, 41	ax-r2 36	. . . . 5 ((a⊥ ∪ b) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))) = (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))
43	16, 42	ax-r2 36	. . . 4 ((a⊥ ∪ (a →4 b)) ∩ (a →4 b)⊥ ) = (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))
44	11, 43	2or 72	. . 3 (((a ∩ (a →4 b)) ∪ (a⊥ ∩ (a →4 b))) ∪ ((a⊥ ∪ (a →4 b)) ∩ (a →4 b)⊥ )) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))))
45		comanr2 465	. . . . . . 7 b C (a ∩ b)
46		comanr2 465	. . . . . . 7 b C (a⊥ ∩ b)
47	45, 46	com2or 483	. . . . . 6 b C ((a ∩ b) ∪ (a⊥ ∩ b))
48		comanr2 465	. . . . . . 7 b⊥ C (a⊥ ∩ b⊥ )
49	48	comcom6 459	. . . . . 6 b C (a⊥ ∩ b⊥ )
50	47, 49	com2or 483	. . . . 5 b C (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
51		comorr2 463	. . . . . . 7 b⊥ C (a⊥ ∪ b⊥ )
52		comorr2 463	. . . . . . 7 b⊥ C (a ∪ b⊥ )
53	51, 52	com2an 484	. . . . . 6 b⊥ C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
54	53	comcom6 459	. . . . 5 b C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
55	50, 54	fh4 472	. . . 4 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))) = (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ b) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))))
56		or32 82	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ b) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b) ∪ (a⊥ ∩ b⊥ ))
57		lear 161	. . . . . . . . . 10 (a ∩ b) ≤ b
58		lear 161	. . . . . . . . . 10 (a⊥ ∩ b) ≤ b
59	57, 58	lel2or 170	. . . . . . . . 9 ((a ∩ b) ∪ (a⊥ ∩ b)) ≤ b
60	59	df-le2 131	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b) = b
61	60	ax-r5 38	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b) ∪ (a⊥ ∩ b⊥ )) = (b ∪ (a⊥ ∩ b⊥ ))
62	56, 61	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ b) = (b ∪ (a⊥ ∩ b⊥ ))
63		comor1 461	. . . . . . . . . . . 12 (a⊥ ∪ b⊥ ) C a⊥
64	63	comcom7 460	. . . . . . . . . . 11 (a⊥ ∪ b⊥ ) C a
65		comor2 462	. . . . . . . . . . . 12 (a⊥ ∪ b⊥ ) C b⊥
66	65	comcom7 460	. . . . . . . . . . 11 (a⊥ ∪ b⊥ ) C b
67	64, 66	com2an 484	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C (a ∩ b)
68	63, 66	com2an 484	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C (a⊥ ∩ b)
69	67, 68	com2or 483	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C ((a ∩ b) ∪ (a⊥ ∩ b))
70	63, 65	com2an 484	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C (a⊥ ∩ b⊥ )
71	69, 70	com2or 483	. . . . . . . 8 (a⊥ ∪ b⊥ ) C (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
72	64, 65	com2or 483	. . . . . . . 8 (a⊥ ∪ b⊥ ) C (a ∪ b⊥ )
73	71, 72	fh4 472	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))) = (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∪ b⊥ )))
74		or32 82	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ ))
75		ax-a3 32	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ )) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b⊥ ) ∪ (a⊥ ∩ b⊥ )))
76		or4 84	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b⊥ ) ∪ (a⊥ ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
77		ax-a2 31	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b) ∪ (a⊥ ∪ b⊥ )))
78		oran3 93	. . . . . . . . . . . . . . . . 17 (a⊥ ∪ b⊥ ) = (a ∩ b)⊥
79	78	lor 70	. . . . . . . . . . . . . . . 16 ((a ∩ b) ∪ (a⊥ ∪ b⊥ )) = ((a ∩ b) ∪ (a ∩ b)⊥ )
80		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a ∩ b) ∪ (a ∩ b)⊥ )
81	80	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a ∩ b) ∪ (a ∩ b)⊥ ) = 1
82	79, 81	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∩ b) ∪ (a⊥ ∪ b⊥ )) = 1
83	82	lor 70	. . . . . . . . . . . . . 14 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b) ∪ (a⊥ ∪ b⊥ ))) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1)
84		or1 104	. . . . . . . . . . . . . 14 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1) = 1
85	83, 84	ax-r2 36	. . . . . . . . . . . . 13 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b) ∪ (a⊥ ∪ b⊥ ))) = 1
86	77, 85	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = 1
87	76, 86	ax-r2 36	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b⊥ ) ∪ (a⊥ ∩ b⊥ ))) = 1
88	75, 87	ax-r2 36	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ )) = 1
89	74, 88	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = 1
90		ax-a3 32	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∪ b⊥ )) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a ∪ b⊥ )))
91		or4 84	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a ∪ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∪ b⊥ )))
92		oran1 91	. . . . . . . . . . . . . . 15 (a ∪ b⊥ ) = (a⊥ ∩ b)⊥
93	92	lor 70	. . . . . . . . . . . . . 14 ((a⊥ ∩ b) ∪ (a ∪ b⊥ )) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
94		df-t 41	. . . . . . . . . . . . . . 15 1 = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
95	94	ax-r1 35	. . . . . . . . . . . . . 14 ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ ) = 1
96	93, 95	ax-r2 36	. . . . . . . . . . . . 13 ((a⊥ ∩ b) ∪ (a ∪ b⊥ )) = 1
97	96	lor 70	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∪ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1)
98		or1 104	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1) = 1
99	97, 98	ax-r2 36	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∪ b⊥ ))) = 1
100	91, 99	ax-r2 36	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a ∪ b⊥ ))) = 1
101	90, 100	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∪ b⊥ )) = 1
102	89, 101	2an 79	. . . . . . . 8 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∪ b⊥ ))) = (1 ∩ 1)
103		an1 106	. . . . . . . 8 (1 ∩ 1) = 1
104	102, 103	ax-r2 36	. . . . . . 7 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∪ b⊥ ))) = 1
105	73, 104	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))) = 1
106	62, 105	2an 79	. . . . 5 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ b) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ 1)
107		an1 106	. . . . . 6 ((b ∪ (a⊥ ∩ b⊥ )) ∩ 1) = (b ∪ (a⊥ ∩ b⊥ ))
108		ax-a2 31	. . . . . 6 (b ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ b)
109	107, 108	ax-r2 36	. . . . 5 ((b ∪ (a⊥ ∩ b⊥ )) ∩ 1) = ((a⊥ ∩ b⊥ ) ∪ b)
110	106, 109	ax-r2 36	. . . 4 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ b) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))) = ((a⊥ ∩ b⊥ ) ∪ b)
111	55, 110	ax-r2 36	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (b ∩ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )))) = ((a⊥ ∩ b⊥ ) ∪ b)
112	44, 111	ax-r2 36	. 2 (((a ∩ (a →4 b)) ∪ (a⊥ ∩ (a →4 b))) ∪ ((a⊥ ∪ (a →4 b)) ∩ (a →4 b)⊥ )) = ((a⊥ ∩ b⊥ ) ∪ b)
113	1, 112	ax-r2 36	1 (a →4 (a →4 b)) = ((a⊥ ∩ b⊥ ) ∪ b)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₄ wi4 15

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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  u4lem5n  766  u4lem6  768