This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid 
 |-  ( 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 )