Metamath Proof Explorer

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	$⊢ A \in V \to suc ⋃ bday [A] \in On$

Proof

Step	Hyp	Ref	Expression
1		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
2		fofun	$⊢ bday : No \underset{onto}{⟶} On \to Fun bday$
3	1 2	ax-mp	$⊢ Fun bday$
4		funimaexg	$⊢ (Fun bday \land A \in V) \to bday [A] \in V$
5	3 4	mpan	$⊢ A \in V \to bday [A] \in V$
6	5	uniexd	$⊢ A \in V \to ⋃ bday [A] \in V$
7		imassrn	$⊢ bday [A] \subseteq ran bday$
8		forn	$⊢ bday : No \underset{onto}{⟶} On \to ran bday = On$
9	1 8	ax-mp	$⊢ ran bday = On$
10	7 9	sseqtri	$⊢ bday [A] \subseteq On$
11		ssorduni	$⊢ bday [A] \subseteq On \to Ord ⋃ bday [A]$
12	10 11	ax-mp	$⊢ Ord ⋃ bday [A]$
13	6 12	jctil	$⊢ A \in V \to (Ord ⋃ bday [A] \land ⋃ bday [A] \in V)$
14		elon2	$⊢ ⋃ bday [A] \in On \leftrightarrow (Ord ⋃ bday [A] \land ⋃ bday [A] \in V)$
15		sucelon	$⊢ ⋃ bday [A] \in On \leftrightarrow suc ⋃ bday [A] \in On$
16	14 15	bitr3i	$⊢ (Ord ⋃ bday [A] \land ⋃ bday [A] \in V) \leftrightarrow suc ⋃ bday [A] \in On$
17	13 16	sylib	$⊢ A \in V \to suc ⋃ bday [A] \in On$