Metamath Proof Explorer

Theorem dfon2

Description: On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011)

Ref Expression
Assertion dfon2 
|- On = { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) }

Proof

Step Hyp Ref Expression
1 df-on 
 |-  On = { x | Ord x }
2 tz7.7 
 |-  ( ( Ord x /\ Tr y ) -> ( y e. x <-> ( y C_ x /\ y =/= x ) ) )
3 df-pss 
 |-  ( y C. x <-> ( y C_ x /\ y =/= x ) )
4 2 3 bitr4di 
 |-  ( ( Ord x /\ Tr y ) -> ( y e. x <-> y C. x ) )
5 4 exbiri 
 |-  ( Ord x -> ( Tr y -> ( y C. x -> y e. x ) ) )
6 5 com23 
 |-  ( Ord x -> ( y C. x -> ( Tr y -> y e. x ) ) )
7 6 impd 
 |-  ( Ord x -> ( ( y C. x /\ Tr y ) -> y e. x ) )
8 7 alrimiv 
 |-  ( Ord x -> A. y ( ( y C. x /\ Tr y ) -> y e. x ) )
9 vex 
 |-  x e. _V
10 dfon2lem3 
 |-  ( x e. _V -> ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) ) )
11 9 10 ax-mp 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) )
12 11 simpld 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr x )
13 9 dfon2lem7 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( t e. x -> A. u ( ( u C. t /\ Tr u ) -> u e. t ) ) )
14 13 ralrimiv 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) )
15 dfon2lem9 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> _E Fr x )
16 psseq2 
 |-  ( t = z -> ( u C. t <-> u C. z ) )
17 16 anbi1d 
 |-  ( t = z -> ( ( u C. t /\ Tr u ) <-> ( u C. z /\ Tr u ) ) )
18 elequ2 
 |-  ( t = z -> ( u e. t <-> u e. z ) )
19 17 18 imbi12d 
 |-  ( t = z -> ( ( ( u C. t /\ Tr u ) -> u e. t ) <-> ( ( u C. z /\ Tr u ) -> u e. z ) ) )
20 19 albidv 
 |-  ( t = z -> ( A. u ( ( u C. t /\ Tr u ) -> u e. t ) <-> A. u ( ( u C. z /\ Tr u ) -> u e. z ) ) )
21 psseq1 
 |-  ( u = v -> ( u C. z <-> v C. z ) )
22 treq 
 |-  ( u = v -> ( Tr u <-> Tr v ) )
23 21 22 anbi12d 
 |-  ( u = v -> ( ( u C. z /\ Tr u ) <-> ( v C. z /\ Tr v ) ) )
24 elequ1 
 |-  ( u = v -> ( u e. z <-> v e. z ) )
25 23 24 imbi12d 
 |-  ( u = v -> ( ( ( u C. z /\ Tr u ) -> u e. z ) <-> ( ( v C. z /\ Tr v ) -> v e. z ) ) )
26 25 cbvalvw 
 |-  ( A. u ( ( u C. z /\ Tr u ) -> u e. z ) <-> A. v ( ( v C. z /\ Tr v ) -> v e. z ) )
27 20 26 bitrdi 
 |-  ( t = z -> ( A. u ( ( u C. t /\ Tr u ) -> u e. t ) <-> A. v ( ( v C. z /\ Tr v ) -> v e. z ) ) )
28 27 rspccv 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> ( z e. x -> A. v ( ( v C. z /\ Tr v ) -> v e. z ) ) )
29 psseq2 
 |-  ( t = w -> ( u C. t <-> u C. w ) )
30 29 anbi1d 
 |-  ( t = w -> ( ( u C. t /\ Tr u ) <-> ( u C. w /\ Tr u ) ) )
31 elequ2 
 |-  ( t = w -> ( u e. t <-> u e. w ) )
32 30 31 imbi12d 
 |-  ( t = w -> ( ( ( u C. t /\ Tr u ) -> u e. t ) <-> ( ( u C. w /\ Tr u ) -> u e. w ) ) )
33 32 albidv 
 |-  ( t = w -> ( A. u ( ( u C. t /\ Tr u ) -> u e. t ) <-> A. u ( ( u C. w /\ Tr u ) -> u e. w ) ) )
34 psseq1 
 |-  ( u = y -> ( u C. w <-> y C. w ) )
35 treq 
 |-  ( u = y -> ( Tr u <-> Tr y ) )
36 34 35 anbi12d 
 |-  ( u = y -> ( ( u C. w /\ Tr u ) <-> ( y C. w /\ Tr y ) ) )
37 elequ1 
 |-  ( u = y -> ( u e. w <-> y e. w ) )
38 36 37 imbi12d 
 |-  ( u = y -> ( ( ( u C. w /\ Tr u ) -> u e. w ) <-> ( ( y C. w /\ Tr y ) -> y e. w ) ) )
39 38 cbvalvw 
 |-  ( A. u ( ( u C. w /\ Tr u ) -> u e. w ) <-> A. y ( ( y C. w /\ Tr y ) -> y e. w ) )
40 33 39 bitrdi 
 |-  ( t = w -> ( A. u ( ( u C. t /\ Tr u ) -> u e. t ) <-> A. y ( ( y C. w /\ Tr y ) -> y e. w ) ) )
41 40 rspccv 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> ( w e. x -> A. y ( ( y C. w /\ Tr y ) -> y e. w ) ) )
42 28 41 anim12d 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> ( ( z e. x /\ w e. x ) -> ( A. v ( ( v C. z /\ Tr v ) -> v e. z ) /\ A. y ( ( y C. w /\ Tr y ) -> y e. w ) ) ) )
43 vex 
 |-  z e. _V
44 vex 
 |-  w e. _V
45 43 44 dfon2lem5 
 |-  ( ( A. v ( ( v C. z /\ Tr v ) -> v e. z ) /\ A. y ( ( y C. w /\ Tr y ) -> y e. w ) ) -> ( z e. w \/ z = w \/ w e. z ) )
46 42 45 syl6 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> ( ( z e. x /\ w e. x ) -> ( z e. w \/ z = w \/ w e. z ) ) )
47 46 ralrimivv 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) )
48 15 47 jca 
 |-  ( A. t e. x A. u ( ( u C. t /\ Tr u ) -> u e. t ) -> ( _E Fr x /\ A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) ) )
49 14 48 syl 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( _E Fr x /\ A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) ) )
50 dfwe2 
 |-  ( _E We x <-> ( _E Fr x /\ A. z e. x A. w e. x ( z _E w \/ z = w \/ w _E z ) ) )
51 epel 
 |-  ( z _E w <-> z e. w )
52 biid 
 |-  ( z = w <-> z = w )
53 epel 
 |-  ( w _E z <-> w e. z )
54 51 52 53 3orbi123i 
 |-  ( ( z _E w \/ z = w \/ w _E z ) <-> ( z e. w \/ z = w \/ w e. z ) )
55 54 2ralbii 
 |-  ( A. z e. x A. w e. x ( z _E w \/ z = w \/ w _E z ) <-> A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) )
56 55 anbi2i 
 |-  ( ( _E Fr x /\ A. z e. x A. w e. x ( z _E w \/ z = w \/ w _E z ) ) <-> ( _E Fr x /\ A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) ) )
57 50 56 bitri 
 |-  ( _E We x <-> ( _E Fr x /\ A. z e. x A. w e. x ( z e. w \/ z = w \/ w e. z ) ) )
58 49 57 sylibr 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> _E We x )
59 df-ord 
 |-  ( Ord x <-> ( Tr x /\ _E We x ) )
60 12 58 59 sylanbrc 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Ord x )
61 8 60 impbii 
 |-  ( Ord x <-> A. y ( ( y C. x /\ Tr y ) -> y e. x ) )
62 61 abbii 
 |-  { x | Ord x } = { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) }
63 1 62 eqtri 
 |-  On = { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) }