Metamath Proof Explorer

Theorem onfr

Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon (through epweon ) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994)

Ref Expression
Assertion onfr 
|- _E Fr On

Proof

Step Hyp Ref Expression
1 dfepfr 
 |-  ( _E Fr On <-> A. x ( ( x C_ On /\ x =/= (/) ) -> E. z e. x ( x i^i z ) = (/) ) )
2 n0 
 |-  ( x =/= (/) <-> E. y y e. x )
3 ineq2 
 |-  ( z = y -> ( x i^i z ) = ( x i^i y ) )
4 3 eqeq1d 
 |-  ( z = y -> ( ( x i^i z ) = (/) <-> ( x i^i y ) = (/) ) )
5 4 rspcev 
 |-  ( ( y e. x /\ ( x i^i y ) = (/) ) -> E. z e. x ( x i^i z ) = (/) )
6 5 adantll 
 |-  ( ( ( x C_ On /\ y e. x ) /\ ( x i^i y ) = (/) ) -> E. z e. x ( x i^i z ) = (/) )
7 inss1 
 |-  ( x i^i y ) C_ x
8 ssel2 
 |-  ( ( x C_ On /\ y e. x ) -> y e. On )
9 eloni 
 |-  ( y e. On -> Ord y )
10 ordfr 
 |-  ( Ord y -> _E Fr y )
11 8 9 10 3syl 
 |-  ( ( x C_ On /\ y e. x ) -> _E Fr y )
12 inss2 
 |-  ( x i^i y ) C_ y
13 vex 
 |-  x e. _V
14 13 inex1 
 |-  ( x i^i y ) e. _V
15 14 epfrc 
 |-  ( ( _E Fr y /\ ( x i^i y ) C_ y /\ ( x i^i y ) =/= (/) ) -> E. z e. ( x i^i y ) ( ( x i^i y ) i^i z ) = (/) )
16 12 15 mp3an2 
 |-  ( ( _E Fr y /\ ( x i^i y ) =/= (/) ) -> E. z e. ( x i^i y ) ( ( x i^i y ) i^i z ) = (/) )
17 11 16 sylan 
 |-  ( ( ( x C_ On /\ y e. x ) /\ ( x i^i y ) =/= (/) ) -> E. z e. ( x i^i y ) ( ( x i^i y ) i^i z ) = (/) )
18 inass 
 |-  ( ( x i^i y ) i^i z ) = ( x i^i ( y i^i z ) )
19 8 9 syl 
 |-  ( ( x C_ On /\ y e. x ) -> Ord y )
20 elinel2 
 |-  ( z e. ( x i^i y ) -> z e. y )
21 ordelss 
 |-  ( ( Ord y /\ z e. y ) -> z C_ y )
22 19 20 21 syl2an 
 |-  ( ( ( x C_ On /\ y e. x ) /\ z e. ( x i^i y ) ) -> z C_ y )
23 sseqin2 
 |-  ( z C_ y <-> ( y i^i z ) = z )
24 22 23 sylib 
 |-  ( ( ( x C_ On /\ y e. x ) /\ z e. ( x i^i y ) ) -> ( y i^i z ) = z )
25 24 ineq2d 
 |-  ( ( ( x C_ On /\ y e. x ) /\ z e. ( x i^i y ) ) -> ( x i^i ( y i^i z ) ) = ( x i^i z ) )
26 18 25 eqtrid 
 |-  ( ( ( x C_ On /\ y e. x ) /\ z e. ( x i^i y ) ) -> ( ( x i^i y ) i^i z ) = ( x i^i z ) )
27 26 eqeq1d 
 |-  ( ( ( x C_ On /\ y e. x ) /\ z e. ( x i^i y ) ) -> ( ( ( x i^i y ) i^i z ) = (/) <-> ( x i^i z ) = (/) ) )
28 27 rexbidva 
 |-  ( ( x C_ On /\ y e. x ) -> ( E. z e. ( x i^i y ) ( ( x i^i y ) i^i z ) = (/) <-> E. z e. ( x i^i y ) ( x i^i z ) = (/) ) )
29 28 adantr 
 |-  ( ( ( x C_ On /\ y e. x ) /\ ( x i^i y ) =/= (/) ) -> ( E. z e. ( x i^i y ) ( ( x i^i y ) i^i z ) = (/) <-> E. z e. ( x i^i y ) ( x i^i z ) = (/) ) )
30 17 29 mpbid 
 |-  ( ( ( x C_ On /\ y e. x ) /\ ( x i^i y ) =/= (/) ) -> E. z e. ( x i^i y ) ( x i^i z ) = (/) )
31 ssrexv 
 |-  ( ( x i^i y ) C_ x -> ( E. z e. ( x i^i y ) ( x i^i z ) = (/) -> E. z e. x ( x i^i z ) = (/) ) )
32 7 30 31 mpsyl 
 |-  ( ( ( x C_ On /\ y e. x ) /\ ( x i^i y ) =/= (/) ) -> E. z e. x ( x i^i z ) = (/) )
33 6 32 pm2.61dane 
 |-  ( ( x C_ On /\ y e. x ) -> E. z e. x ( x i^i z ) = (/) )
34 33 ex 
 |-  ( x C_ On -> ( y e. x -> E. z e. x ( x i^i z ) = (/) ) )
35 34 exlimdv 
 |-  ( x C_ On -> ( E. y y e. x -> E. z e. x ( x i^i z ) = (/) ) )
36 2 35 syl5bi 
 |-  ( x C_ On -> ( x =/= (/) -> E. z e. x ( x i^i z ) = (/) ) )
37 36 imp 
 |-  ( ( x C_ On /\ x =/= (/) ) -> E. z e. x ( x i^i z ) = (/) )
38 1 37 mpgbir 
 |-  _E Fr On