Theorem hfuniOLD

Description: Obsolete version of hfuni as of 17-Sep-2026. (Contributed by Scott Fenton, 16-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfuniOLD	Could not format assertion : No typesetting found for |- ( A e. HF -> U. A e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rankuni	$$⊢\mathrm{rank}\left(\bigcup A\right)=\bigcup \mathrm{rank}\left(A\right)$$
2		rankon	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{On}$$
3		ontr	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{On}\to \mathrm{Tr}\mathrm{rank}\left(A\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Tr}\mathrm{rank}\left(A\right)$$
5		df-tr	$$⊢\mathrm{Tr}\mathrm{rank}\left(A\right)\leftrightarrow \bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)$$
6	4 5	mpbi	$$⊢\bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)$$
7		elhf2g	Could not format ( A e. HF -> ( A e. HF <-> ( rank ` A ) e. _om ) ) : No typesetting found for |- ( A e. HF -> ( A e. HF <-> ( rank ` A ) e. _om ) ) with typecode |-
8	7	ibi	Could not format ( A e. HF -> ( rank ` A ) e. _om ) : No typesetting found for |- ( A e. HF -> ( rank ` A ) e. _om ) with typecode |-
9		rankon	$$⊢\mathrm{rank}\left(\bigcup A\right)\in \mathrm{On}$$
10	1 9	eqeltrri	$$⊢\bigcup \mathrm{rank}\left(A\right)\in \mathrm{On}$$
11	10	onordi	$$⊢\mathrm{Ord}\bigcup \mathrm{rank}\left(A\right)$$
12		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
13		ordtr2	$$⊢\left(\mathrm{Ord}\bigcup \mathrm{rank}\left(A\right)\wedge \mathrm{Ord}\mathrm{\omega }\right)\to \left(\left(\bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)\wedge \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)\to \bigcup \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)$$
14	11 12 13	mp2an	$$⊢\left(\bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)\wedge \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)\to \bigcup \mathrm{rank}\left(A\right)\in \mathrm{\omega }$$
15	6 8 14	sylancr	Could not format ( A e. HF -> U. ( rank ` A ) e. _om ) : No typesetting found for |- ( A e. HF -> U. ( rank ` A ) e. _om ) with typecode |-
16	1 15	eqeltrid	Could not format ( A e. HF -> ( rank ` U. A ) e. _om ) : No typesetting found for |- ( A e. HF -> ( rank ` U. A ) e. _om ) with typecode |-
17		uniexg	Could not format ( A e. HF -> U. A e. _V ) : No typesetting found for |- ( A e. HF -> U. A e. _V ) with typecode |-
18		elhf2g	Could not format ( U. A e. _V -> ( U. A e. HF <-> ( rank ` U. A ) e. _om ) ) : No typesetting found for |- ( U. A e. _V -> ( U. A e. HF <-> ( rank ` U. A ) e. _om ) ) with typecode |-
19	17 18	syl	Could not format ( A e. HF -> ( U. A e. HF <-> ( rank ` U. A ) e. _om ) ) : No typesetting found for |- ( A e. HF -> ( U. A e. HF <-> ( rank ` U. A ) e. _om ) ) with typecode |-
20	16 19	mpbird	Could not format ( A e. HF -> U. A e. HF ) : No typesetting found for |- ( A e. HF -> U. A e. HF ) with typecode |-