hartogs

Description: Given any set, the Hartogs number of the set is the least ordinal not dominated by that set. This theorem proves that there is always an ordinal which satisfies this. (This theorem can be proven trivially using the AC - see theorem ondomon - but this proof works in ZF.) (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 )

Metamath Proof Explorer

Theorem hartogs

Proof