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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On )

Proof

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