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 | y y x Tr y y x

Proof

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