Theorem hartogs

Description: The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 and hartogslem2 ) proof can be given using the axiom of choice, see ondomon . As its label indicates, this result is used to justify the definition of the Hartogs function df-har . (Contributed by Jeff Hankins, 22-Oct-2009) (Revised by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	hartogs	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 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		eqid	⊢ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
29		eqid	⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑔 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑔 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑔 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑔 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
30	28 29	hartogslem2	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ V )
31		elong	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ V → ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
32	30 31	syl	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) )
33	27 32	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On )