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|∀yy⊂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→∀yy⊂x∧Tr⁡y→y∈x
9 vex ⊢x∈V
10 dfon2lem3 ⊢x∈V→∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x∧∀z∈x¬z∈z
11 9 10 ax-mp ⊢∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x∧∀z∈x¬z∈z
12 11 simpld ⊢∀yy⊂x∧Tr⁡y→y∈x→Tr⁡x
13 9 dfon2lem7 ⊢∀yy⊂x∧Tr⁡y→y∈x→t∈x→∀uu⊂t∧Tr⁡u→u∈t
14 13 ralrimiv ⊢∀yy⊂x∧Tr⁡y→y∈x→∀t∈x∀uu⊂t∧Tr⁡u→u∈t
15 dfon2lem9 ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→EFrx
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→∀uu⊂t∧Tr⁡u→u∈t↔∀uu⊂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 ⊢∀uu⊂z∧Tr⁡u→u∈z↔∀vv⊂z∧Tr⁡v→v∈z
27 20 26 bitrdi ⊢t=z→∀uu⊂t∧Tr⁡u→u∈t↔∀vv⊂z∧Tr⁡v→v∈z
28 27 rspccv ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→z∈x→∀vv⊂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→∀uu⊂t∧Tr⁡u→u∈t↔∀uu⊂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 ⊢∀uu⊂w∧Tr⁡u→u∈w↔∀yy⊂w∧Tr⁡y→y∈w
40 33 39 bitrdi ⊢t=w→∀uu⊂t∧Tr⁡u→u∈t↔∀yy⊂w∧Tr⁡y→y∈w
41 40 rspccv ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→w∈x→∀yy⊂w∧Tr⁡y→y∈w
42 28 41 anim12d ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→z∈x∧w∈x→∀vv⊂z∧Tr⁡v→v∈z∧∀yy⊂w∧Tr⁡y→y∈w
43 vex ⊢z∈V
44 vex ⊢w∈V
45 43 44 dfon2lem5 ⊢∀vv⊂z∧Tr⁡v→v∈z∧∀yy⊂w∧Tr⁡y→y∈w→z∈w∨z=w∨w∈z
46 42 45 syl6 ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→z∈x∧w∈x→z∈w∨z=w∨w∈z
47 46 ralrimivv ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→∀z∈x∀w∈xz∈w∨z=w∨w∈z
48 15 47 jca ⊢∀t∈x∀uu⊂t∧Tr⁡u→u∈t→EFrx∧∀z∈x∀w∈xz∈w∨z=w∨w∈z
49 14 48 syl ⊢∀yy⊂x∧Tr⁡y→y∈x→EFrx∧∀z∈x∀w∈xz∈w∨z=w∨w∈z
50 dfwe2 ⊢EWex↔EFrx∧∀z∈x∀w∈xzEw∨z=w∨wEz
51 epel ⊢zEw↔z∈w
52 biid ⊢z=w↔z=w
53 epel ⊢wEz↔w∈z
54 51 52 53 3orbi123i ⊢zEw∨z=w∨wEz↔z∈w∨z=w∨w∈z
55 54 2ralbii ⊢∀z∈x∀w∈xzEw∨z=w∨wEz↔∀z∈x∀w∈xz∈w∨z=w∨w∈z
56 55 anbi2i ⊢EFrx∧∀z∈x∀w∈xzEw∨z=w∨wEz↔EFrx∧∀z∈x∀w∈xz∈w∨z=w∨w∈z
57 50 56 bitri ⊢EWex↔EFrx∧∀z∈x∀w∈xz∈w∨z=w∨w∈z
58 49 57 sylibr ⊢∀yy⊂x∧Tr⁡y→y∈x→EWex
59 df-ord ⊢Ord⁡x↔Tr⁡x∧EWex
60 12 58 59 sylanbrc ⊢∀yy⊂x∧Tr⁡y→y∈x→Ord⁡x
61 8 60 impbii ⊢Ord⁡x↔∀yy⊂x∧Tr⁡y→y∈x
62 61 abbii ⊢x|Ord⁡x=x|∀yy⊂x∧Tr⁡y→y∈x
63 1 62 eqtri ⊢On=x|∀yy⊂x∧Tr⁡y→y∈x