Metamath Proof Explorer

Theorem dfon2lem9

Description: Lemma for dfon2 . A class of new ordinals is well-founded by _E . (Contributed by Scott Fenton, 3-Mar-2011)

Ref Expression
Assertion dfon2lem9 
|- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> _E Fr A )

Proof

Step Hyp Ref Expression
1 ssralv 
 |-  ( z C_ A -> ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) )
2 dfon2lem8 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) /\ |^| z e. z ) )
3 2 simprd 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> |^| z e. z )
4 intss1 
 |-  ( t e. z -> |^| z C_ t )
5 2 simpld 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) )
6 intex 
 |-  ( z =/= (/) <-> |^| z e. _V )
7 dfon2lem3 
 |-  ( |^| z e. _V -> ( A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) -> ( Tr |^| z /\ A. x e. |^| z -. x e. x ) ) )
8 7 imp 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( Tr |^| z /\ A. x e. |^| z -. x e. x ) )
9 8 simprd 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> A. x e. |^| z -. x e. x )
10 untelirr 
 |-  ( A. x e. |^| z -. x e. x -> -. |^| z e. |^| z )
11 9 10 syl 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> -. |^| z e. |^| z )
12 eleq1 
 |-  ( |^| z = t -> ( |^| z e. |^| z <-> t e. |^| z ) )
13 12 notbid 
 |-  ( |^| z = t -> ( -. |^| z e. |^| z <-> -. t e. |^| z ) )
14 11 13 syl5ibcom 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z = t -> -. t e. |^| z ) )
15 14 a1dd 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z = t -> ( |^| z C_ t -> -. t e. |^| z ) ) )
16 8 simpld 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> Tr |^| z )
17 trss 
 |-  ( Tr |^| z -> ( t e. |^| z -> t C_ |^| z ) )
18 16 17 syl 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( t e. |^| z -> t C_ |^| z ) )
19 eqss 
 |-  ( |^| z = t <-> ( |^| z C_ t /\ t C_ |^| z ) )
20 19 simplbi2com 
 |-  ( t C_ |^| z -> ( |^| z C_ t -> |^| z = t ) )
21 18 20 syl6 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( t e. |^| z -> ( |^| z C_ t -> |^| z = t ) ) )
22 21 com23 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z C_ t -> ( t e. |^| z -> |^| z = t ) ) )
23 con3 
 |-  ( ( t e. |^| z -> |^| z = t ) -> ( -. |^| z = t -> -. t e. |^| z ) )
24 22 23 syl6 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z C_ t -> ( -. |^| z = t -> -. t e. |^| z ) ) )
25 24 com23 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( -. |^| z = t -> ( |^| z C_ t -> -. t e. |^| z ) ) )
26 15 25 pm2.61d 
 |-  ( ( |^| z e. _V /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z C_ t -> -. t e. |^| z ) )
27 6 26 sylanb 
 |-  ( ( z =/= (/) /\ A. u ( ( u C. |^| z /\ Tr u ) -> u e. |^| z ) ) -> ( |^| z C_ t -> -. t e. |^| z ) )
28 5 27 syldan 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( |^| z C_ t -> -. t e. |^| z ) )
29 4 28 syl5 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. z -> -. t e. |^| z ) )
30 29 ralrimiv 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. t e. z -. t e. |^| z )
31 eleq2 
 |-  ( w = |^| z -> ( t e. w <-> t e. |^| z ) )
32 31 notbid 
 |-  ( w = |^| z -> ( -. t e. w <-> -. t e. |^| z ) )
33 32 ralbidv 
 |-  ( w = |^| z -> ( A. t e. z -. t e. w <-> A. t e. z -. t e. |^| z ) )
34 33 rspcev 
 |-  ( ( |^| z e. z /\ A. t e. z -. t e. |^| z ) -> E. w e. z A. t e. z -. t e. w )
35 3 30 34 syl2anc 
 |-  ( ( z =/= (/) /\ A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> E. w e. z A. t e. z -. t e. w )
36 35 expcom 
 |-  ( A. x e. z A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( z =/= (/) -> E. w e. z A. t e. z -. t e. w ) )
37 1 36 syl6com 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( z C_ A -> ( z =/= (/) -> E. w e. z A. t e. z -. t e. w ) ) )
38 37 impd 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t e. w ) )
39 38 alrimiv 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. z ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t e. w ) )
40 df-fr 
 |-  ( _E Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t _E w ) )
41 epel 
 |-  ( t _E w <-> t e. w )
42 41 notbii 
 |-  ( -. t _E w <-> -. t e. w )
43 42 ralbii 
 |-  ( A. t e. z -. t _E w <-> A. t e. z -. t e. w )
44 43 rexbii 
 |-  ( E. w e. z A. t e. z -. t _E w <-> E. w e. z A. t e. z -. t e. w )
45 44 imbi2i 
 |-  ( ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t _E w ) <-> ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t e. w ) )
46 45 albii 
 |-  ( A. z ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t _E w ) <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t e. w ) )
47 40 46 bitri 
 |-  ( _E Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. w e. z A. t e. z -. t e. w ) )
48 39 47 sylibr 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> _E Fr A )