Theorem untsucf

Description: If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	untsucf.1	|- F/_ y A
Assertion	untsucf	|- ( A. x e. A -. x e. x -> A. y e. suc A -. y e. y )

Proof

Step	Hyp	Ref	Expression
1		untsucf.1	|- F/_ y A
2		nfv	|- F/ y -. x e. x
3	1 2	nfralw	|- F/ y A. x e. A -. x e. x
4		vex	|- y e. _V
5	4	elsuc	|- ( y e. suc A <-> ( y e. A \/ y = A ) )
6		elequ1	|- ( x = y -> ( x e. x <-> y e. x ) )
7		elequ2	|- ( x = y -> ( y e. x <-> y e. y ) )
8	6 7	bitrd	|- ( x = y -> ( x e. x <-> y e. y ) )
9	8	notbid	|- ( x = y -> ( -. x e. x <-> -. y e. y ) )
10	9	rspccv	|- ( A. x e. A -. x e. x -> ( y e. A -> -. y e. y ) )
11		untelirr	|- ( A. x e. A -. x e. x -> -. A e. A )
12		eleq1	|- ( y = A -> ( y e. y <-> A e. y ) )
13		eleq2	|- ( y = A -> ( A e. y <-> A e. A ) )
14	12 13	bitrd	|- ( y = A -> ( y e. y <-> A e. A ) )
15	14	notbid	|- ( y = A -> ( -. y e. y <-> -. A e. A ) )
16	11 15	syl5ibrcom	|- ( A. x e. A -. x e. x -> ( y = A -> -. y e. y ) )
17	10 16	jaod	|- ( A. x e. A -. x e. x -> ( ( y e. A \/ y = A ) -> -. y e. y ) )
18	5 17	syl5bi	|- ( A. x e. A -. x e. x -> ( y e. suc A -> -. y e. y ) )
19	3 18	ralrimi	|- ( A. x e. A -. x e. x -> A. y e. suc A -. y e. y )