Theorem bdayimaon

Description: Lemma for full-eta properties. The successor of the union of the image of the birthday function under a set is an ordinal. (Contributed by Scott Fenton, 20-Aug-2011)

	Ref	Expression
Assertion	bdayimaon	⊢ ( 𝐴 ∈ 𝑉 → suc ∪ ( bday “ 𝐴 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		bdayfo	⊢ bday : No –onto→ On
2		fofun	⊢ ( bday : No –onto→ On → Fun bday )
3	1 2	ax-mp	⊢ Fun bday
4		funimaexg	⊢ ( ( Fun bday ∧ 𝐴 ∈ 𝑉 ) → ( bday “ 𝐴 ) ∈ V )
5	3 4	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( bday “ 𝐴 ) ∈ V )
6	5	uniexd	⊢ ( 𝐴 ∈ 𝑉 → ∪ ( bday “ 𝐴 ) ∈ V )
7		imassrn	⊢ ( bday “ 𝐴 ) ⊆ ran bday
8		forn	⊢ ( bday : No –onto→ On → ran bday = On )
9	1 8	ax-mp	⊢ ran bday = On
10	7 9	sseqtri	⊢ ( bday “ 𝐴 ) ⊆ On
11		ssorduni	⊢ ( ( bday “ 𝐴 ) ⊆ On → Ord ∪ ( bday “ 𝐴 ) )
12	10 11	ax-mp	⊢ Ord ∪ ( bday “ 𝐴 )
13	6 12	jctil	⊢ ( 𝐴 ∈ 𝑉 → ( Ord ∪ ( bday “ 𝐴 ) ∧ ∪ ( bday “ 𝐴 ) ∈ V ) )
14		elon2	⊢ ( ∪ ( bday “ 𝐴 ) ∈ On ↔ ( Ord ∪ ( bday “ 𝐴 ) ∧ ∪ ( bday “ 𝐴 ) ∈ V ) )
15		sucelon	⊢ ( ∪ ( bday “ 𝐴 ) ∈ On ↔ suc ∪ ( bday “ 𝐴 ) ∈ On )
16	14 15	bitr3i	⊢ ( ( Ord ∪ ( bday “ 𝐴 ) ∧ ∪ ( bday “ 𝐴 ) ∈ V ) ↔ suc ∪ ( bday “ 𝐴 ) ∈ On )
17	13 16	sylib	⊢ ( 𝐴 ∈ 𝑉 → suc ∪ ( bday “ 𝐴 ) ∈ On )