This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑦 ) → 𝑦 ∈ 𝑥 ) }