Metamath Proof Explorer

Theorem ondomon

Description: The class of ordinals dominated by a given set is an ordinal. Theorem 56 of Suppes p. 227. This theorem can be proved without the axiom of choice, see hartogs . (Contributed by NM, 7-Nov-2003) (Proof modification is discouraged.) Use hartogs instead. (New usage is discouraged.)

Ref Expression
Assertion ondomon ⊢ A ∈ V → x ∈ On | x ≼ A ∈ On

Proof

Step Hyp Ref Expression
1 onelon ⊢ z ∈ On ∧ y ∈ z → y ∈ On
2 vex ⊢ z ∈ V
3 onelss ⊢ z ∈ On → y ∈ z → y ⊆ z
4 3 imp ⊢ z ∈ On ∧ y ∈ z → y ⊆ z
5 ssdomg ⊢ z ∈ V → y ⊆ z → y ≼ z
6 2 4 5 mpsyl ⊢ z ∈ On ∧ y ∈ z → y ≼ z
7 1 6 jca ⊢ z ∈ On ∧ y ∈ z → y ∈ On ∧ y ≼ z
8 domtr ⊢ y ≼ z ∧ z ≼ A → y ≼ A
9 8 anim2i ⊢ y ∈ On ∧ y ≼ z ∧ z ≼ A → y ∈ On ∧ y ≼ A
10 9 anassrs ⊢ y ∈ On ∧ y ≼ z ∧ z ≼ A → y ∈ On ∧ y ≼ A
11 7 10 sylan ⊢ z ∈ On ∧ y ∈ z ∧ z ≼ A → y ∈ On ∧ y ≼ A
12 11 exp31 ⊢ z ∈ On → y ∈ z → z ≼ A → y ∈ On ∧ y ≼ A
13 12 com12 ⊢ y ∈ z → z ∈ On → z ≼ A → y ∈ On ∧ y ≼ A
14 13 impd ⊢ y ∈ z → z ∈ On ∧ z ≼ A → y ∈ On ∧ y ≼ A
15 breq1 ⊢ x = z → x ≼ A ↔ z ≼ A
16 15 elrab ⊢ z ∈ x ∈ On | x ≼ A ↔ z ∈ On ∧ z ≼ A
17 breq1 ⊢ x = y → x ≼ A ↔ y ≼ A
18 17 elrab ⊢ y ∈ x ∈ On | x ≼ A ↔ y ∈ On ∧ y ≼ A
19 14 16 18 3imtr4g ⊢ y ∈ z → z ∈ x ∈ On | x ≼ A → y ∈ x ∈ On | x ≼ A
20 19 imp ⊢ y ∈ z ∧ z ∈ x ∈ On | x ≼ A → y ∈ x ∈ On | x ≼ A
21 20 gen2 ⊢ ∀ y ∀ z y ∈ z ∧ z ∈ x ∈ On | x ≼ A → y ∈ x ∈ On | x ≼ A
22 dftr2 ⊢ Tr ⁡ x ∈ On | x ≼ A ↔ ∀ y ∀ z y ∈ z ∧ z ∈ x ∈ On | x ≼ A → y ∈ x ∈ On | x ≼ A
23 21 22 mpbir ⊢ Tr ⁡ x ∈ On | x ≼ A
24 ssrab2 ⊢ x ∈ On | x ≼ A ⊆ On
25 ordon ⊢ Ord ⁡ On
26 trssord ⊢ Tr ⁡ x ∈ On | x ≼ A ∧ x ∈ On | x ≼ A ⊆ On ∧ Ord ⁡ On → Ord ⁡ x ∈ On | x ≼ A
27 23 24 25 26 mp3an ⊢ Ord ⁡ x ∈ On | x ≼ A
28 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
29 numth3 ⊢ 𝒫 A ∈ V → 𝒫 A ∈ dom ⁡ card
30 cardval2 ⊢ 𝒫 A ∈ dom ⁡ card → card ⁡ 𝒫 A = x ∈ On | x ≺ 𝒫 A
31 28 29 30 3syl ⊢ A ∈ V → card ⁡ 𝒫 A = x ∈ On | x ≺ 𝒫 A
32 fvex ⊢ card ⁡ 𝒫 A ∈ V
33 31 32 eqeltrrdi ⊢ A ∈ V → x ∈ On | x ≺ 𝒫 A ∈ V
34 elex ⊢ A ∈ V → A ∈ V
35 canth2g ⊢ A ∈ V → A ≺ 𝒫 A
36 domsdomtr ⊢ x ≼ A ∧ A ≺ 𝒫 A → x ≺ 𝒫 A
37 35 36 sylan2 ⊢ x ≼ A ∧ A ∈ V → x ≺ 𝒫 A
38 37 expcom ⊢ A ∈ V → x ≼ A → x ≺ 𝒫 A
39 38 ralrimivw ⊢ A ∈ V → ∀ x ∈ On x ≼ A → x ≺ 𝒫 A
40 34 39 syl ⊢ A ∈ V → ∀ x ∈ On x ≼ A → x ≺ 𝒫 A
41 40 ss2rabd ⊢ A ∈ V → x ∈ On | x ≼ A ⊆ x ∈ On | x ≺ 𝒫 A
42 33 41 ssexd ⊢ A ∈ V → x ∈ On | x ≼ A ∈ V
43 elong ⊢ x ∈ On | x ≼ A ∈ V → x ∈ On | x ≼ A ∈ On ↔ Ord ⁡ x ∈ On | x ≼ A
44 42 43 syl ⊢ A ∈ V → x ∈ On | x ≼ A ∈ On ↔ Ord ⁡ x ∈ On | x ≼ A
45 27 44 mpbiri ⊢ A ∈ V → x ∈ On | x ≼ A ∈ On