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