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 = { 𝑥 ∣ ∀ 𝑦 ( ( 𝑦𝑥 ∧ Tr 𝑦 ) → 𝑦𝑥 ) }

Proof

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