Theorem axacprim

Description: ax-ac without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010)

	Ref	Expression
Assertion	axacprim	|- -. A. x -. A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axacnd	|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
2		df-an	|- ( ( y e. z /\ z e. w ) <-> -. ( y e. z -> -. z e. w ) )
3	2	albii	|- ( A. x ( y e. z /\ z e. w ) <-> A. x -. ( y e. z -> -. z e. w ) )
4		anass	|- ( ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> ( y e. z /\ ( z e. w /\ ( y e. w /\ w e. x ) ) ) )
5		annim	|- ( ( z e. w /\ -. ( y e. w -> -. w e. x ) ) <-> -. ( z e. w -> ( y e. w -> -. w e. x ) ) )
6		pm4.63	|- ( -. ( y e. w -> -. w e. x ) <-> ( y e. w /\ w e. x ) )
7	6	anbi2i	|- ( ( z e. w /\ -. ( y e. w -> -. w e. x ) ) <-> ( z e. w /\ ( y e. w /\ w e. x ) ) )
8	5 7	bitr3i	|- ( -. ( z e. w -> ( y e. w -> -. w e. x ) ) <-> ( z e. w /\ ( y e. w /\ w e. x ) ) )
9	8	anbi2i	|- ( ( y e. z /\ -. ( z e. w -> ( y e. w -> -. w e. x ) ) ) <-> ( y e. z /\ ( z e. w /\ ( y e. w /\ w e. x ) ) ) )
10		annim	|- ( ( y e. z /\ -. ( z e. w -> ( y e. w -> -. w e. x ) ) ) <-> -. ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) )
11	4 9 10	3bitr2i	|- ( ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> -. ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) )
12	11	exbii	|- ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> E. w -. ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) )
13		exnal	|- ( E. w -. ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) <-> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) )
14	12 13	bitri	|- ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) )
15	14	bibi1i	|- ( ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) <-> y = w ) )
16		dfbi1	|- ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) <-> y = w ) <-> -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
17	15 16	bitri	|- ( ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
18	17	albii	|- ( A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
19	18	exbii	|- ( E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> E. w A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
20		df-ex	|- ( E. w A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) <-> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
21	19 20	bitri	|- ( E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )
22	3 21	imbi12i	|- ( ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) )
23	22	2albii	|- ( A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) )
24	23	exbii	|- ( E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> E. x A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) )
25		df-ex	|- ( E. x A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) <-> -. A. x -. A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) )
26	24 25	bitri	|- ( E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> -. A. x -. A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) ) )
27	1 26	mpbi	|- -. A. x -. A. y A. z ( A. x -. ( y e. z -> -. z e. w ) -> -. A. w -. A. y -. ( ( -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) -> y = w ) -> -. ( y = w -> -. A. w ( y e. z -> ( z e. w -> ( y e. w -> -. w e. x ) ) ) ) ) )