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

Metamath Proof Explorer

Theorem tz9.13

Description: Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of TakeutiZaring p. 78. (Contributed by NM, 23-Sep-2003)

Ref Expression
Hypothesis tz9.13.1 
|- A e. _V
Assertion tz9.13 
|- E. x e. On A e. ( R1 ` x )

Proof

Step Hyp Ref Expression
1 tz9.13.1 
 |-  A e. _V
2 setind 
 |-  ( A. z ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> z e. { y | E. x e. On y e. ( R1 ` x ) } ) -> { y | E. x e. On y e. ( R1 ` x ) } = _V )
3 ssel 
 |-  ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> ( w e. z -> w e. { y | E. x e. On y e. ( R1 ` x ) } ) )
4 vex 
 |-  w e. _V
5 eleq1 
 |-  ( y = w -> ( y e. ( R1 ` x ) <-> w e. ( R1 ` x ) ) )
6 5 rexbidv 
 |-  ( y = w -> ( E. x e. On y e. ( R1 ` x ) <-> E. x e. On w e. ( R1 ` x ) ) )
7 4 6 elab 
 |-  ( w e. { y | E. x e. On y e. ( R1 ` x ) } <-> E. x e. On w e. ( R1 ` x ) )
8 3 7 imbitrdi 
 |-  ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> ( w e. z -> E. x e. On w e. ( R1 ` x ) ) )
9 8 ralrimiv 
 |-  ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> A. w e. z E. x e. On w e. ( R1 ` x ) )
10 vex 
 |-  z e. _V
11 10 tz9.12 
 |-  ( A. w e. z E. x e. On w e. ( R1 ` x ) -> E. x e. On z e. ( R1 ` x ) )
12 9 11 syl 
 |-  ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> E. x e. On z e. ( R1 ` x ) )
13 eleq1 
 |-  ( y = z -> ( y e. ( R1 ` x ) <-> z e. ( R1 ` x ) ) )
14 13 rexbidv 
 |-  ( y = z -> ( E. x e. On y e. ( R1 ` x ) <-> E. x e. On z e. ( R1 ` x ) ) )
15 10 14 elab 
 |-  ( z e. { y | E. x e. On y e. ( R1 ` x ) } <-> E. x e. On z e. ( R1 ` x ) )
16 12 15 sylibr 
 |-  ( z C_ { y | E. x e. On y e. ( R1 ` x ) } -> z e. { y | E. x e. On y e. ( R1 ` x ) } )
17 2 16 mpg 
 |-  { y | E. x e. On y e. ( R1 ` x ) } = _V
18 1 17 eleqtrri 
 |-  A e. { y | E. x e. On y e. ( R1 ` x ) }
19 eleq1 
 |-  ( y = A -> ( y e. ( R1 ` x ) <-> A e. ( R1 ` x ) ) )
20 19 rexbidv 
 |-  ( y = A -> ( E. x e. On y e. ( R1 ` x ) <-> E. x e. On A e. ( R1 ` x ) ) )
21 1 20 elab 
 |-  ( A e. { y | E. x e. On y e. ( R1 ` x ) } <-> E. x e. On A e. ( R1 ` x ) )
22 18 21 mpbi 
 |-  E. x e. On A e. ( R1 ` x )