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 elex ⊢ A ∈ V → A ∈ V
29 canth2g ⊢ A ∈ V → A ≺ 𝒫 A
30 domsdomtr ⊢ x ≼ A ∧ A ≺ 𝒫 A → x ≺ 𝒫 A
31 29 30 sylan2 ⊢ x ≼ A ∧ A ∈ V → x ≺ 𝒫 A
32 31 expcom ⊢ A ∈ V → x ≼ A → x ≺ 𝒫 A
33 32 ralrimivw ⊢ A ∈ V → ∀ x ∈ On x ≼ A → x ≺ 𝒫 A
34 28 33 syl ⊢ A ∈ V → ∀ x ∈ On x ≼ A → x ≺ 𝒫 A
35 ss2rab ⊢ x ∈ On | x ≼ A ⊆ x ∈ On | x ≺ 𝒫 A ↔ ∀ x ∈ On x ≼ A → x ≺ 𝒫 A
36 34 35 sylibr ⊢ A ∈ V → x ∈ On | x ≼ A ⊆ x ∈ On | x ≺ 𝒫 A
37 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
38 numth3 ⊢ 𝒫 A ∈ V → 𝒫 A ∈ dom ⁡ card
39 cardval2 ⊢ 𝒫 A ∈ dom ⁡ card → card ⁡ 𝒫 A = x ∈ On | x ≺ 𝒫 A
40 37 38 39 3syl ⊢ A ∈ V → card ⁡ 𝒫 A = x ∈ On | x ≺ 𝒫 A
41 fvex ⊢ card ⁡ 𝒫 A ∈ V
42 40 41 eqeltrrdi ⊢ A ∈ V → x ∈ On | x ≺ 𝒫 A ∈ V
43 ssexg ⊢ x ∈ On | x ≼ A ⊆ x ∈ On | x ≺ 𝒫 A ∧ x ∈ On | x ≺ 𝒫 A ∈ V → x ∈ On | x ≼ A ∈ V
44 36 42 43 syl2anc ⊢ A ∈ V → x ∈ On | x ≼ A ∈ V
45 elong ⊢ x ∈ On | x ≼ A ∈ V → x ∈ On | x ≼ A ∈ On ↔ Ord ⁡ x ∈ On | x ≼ A
46 44 45 syl ⊢ A ∈ V → x ∈ On | x ≼ A ∈ On ↔ Ord ⁡ x ∈ On | x ≼ A
47 27 46 mpbiri ⊢ A ∈ V → x ∈ On | x ≼ A ∈ On