Theorem axinfprim

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

	Ref	Expression
Assertion	axinfprim	|- -. A. x -. ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axinfnd	|- E. x ( y e. z -> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
2		df-an	|- ( ( y e. z /\ z e. x ) <-> -. ( y e. z -> -. z e. x ) )
3	2	exbii	|- ( E. z ( y e. z /\ z e. x ) <-> E. z -. ( y e. z -> -. z e. x ) )
4		exnal	|- ( E. z -. ( y e. z -> -. z e. x ) <-> -. A. z ( y e. z -> -. z e. x ) )
5	3 4	bitri	|- ( E. z ( y e. z /\ z e. x ) <-> -. A. z ( y e. z -> -. z e. x ) )
6	5	imbi2i	|- ( ( y e. x -> E. z ( y e. z /\ z e. x ) ) <-> ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) )
7	6	albii	|- ( A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) <-> A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) )
8	7	anbi2i	|- ( ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) <-> ( y e. x /\ A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )
9		df-an	|- ( ( y e. x /\ A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) <-> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )
10	8 9	bitri	|- ( ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) <-> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )
11	10	imbi2i	|- ( ( y e. z -> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) ) <-> ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) ) )
12	11	exbii	|- ( E. x ( y e. z -> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) ) <-> E. x ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) ) )
13		df-ex	|- ( E. x ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) ) <-> -. A. x -. ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) ) )
14	12 13	bitri	|- ( E. x ( y e. z -> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) ) <-> -. A. x -. ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) ) )
15	1 14	mpbi	|- -. A. x -. ( y e. z -> -. ( y e. x -> -. A. y ( y e. x -> -. A. z ( y e. z -> -. z e. x ) ) ) )