Theorem hfunOLD

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

	Ref	Expression
Assertion	hfunOLD	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		rankung	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
2		elhf2g	⊢ ( 𝐴 ∈ HF → ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
3	2	ibi	⊢ ( 𝐴 ∈ HF → ( rank ‘ 𝐴 ) ∈ ω )
4		elhf2g	⊢ ( 𝐵 ∈ HF → ( 𝐵 ∈ HF ↔ ( rank ‘ 𝐵 ) ∈ ω ) )
5	4	ibi	⊢ ( 𝐵 ∈ HF → ( rank ‘ 𝐵 ) ∈ ω )
6		eleq1a	⊢ ( ( rank ‘ 𝐵 ) ∈ ω → ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐵 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω ) )
7	6	adantl	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐵 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω ) )
8		uncom	⊢ ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
9	8	eqeq1i	⊢ ( ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) ↔ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐴 ) )
10	9	biimpi	⊢ ( ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐴 ) )
11	10	eleq1d	⊢ ( ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) → ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
12	11	biimprcd	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → ( ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω ) )
13	12	adantr	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω ) )
14		nnord	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → Ord ( rank ‘ 𝐴 ) )
15		nnord	⊢ ( ( rank ‘ 𝐵 ) ∈ ω → Ord ( rank ‘ 𝐵 ) )
16		ordtri2or2	⊢ ( ( Ord ( rank ‘ 𝐴 ) ∧ Ord ( rank ‘ 𝐵 ) ) → ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ∨ ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ) )
17	14 15 16	syl2an	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ∨ ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ) )
18		ssequn1	⊢ ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ↔ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐵 ) )
19		ssequn1	⊢ ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ↔ ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) )
20	18 19	orbi12i	⊢ ( ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ∨ ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ) ↔ ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐵 ) ∨ ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) ) )
21	17 20	sylib	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( rank ‘ 𝐵 ) ∨ ( ( rank ‘ 𝐵 ) ∪ ( rank ‘ 𝐴 ) ) = ( rank ‘ 𝐴 ) ) )
22	7 13 21	mpjaod	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ( rank ‘ 𝐵 ) ∈ ω ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω )
23	3 5 22	syl2an	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ω )
24	1 23	eqeltrd	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ω )
25		unexg	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
26		elhf2g	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( ( 𝐴 ∪ 𝐵 ) ∈ HF ↔ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ω ) )
27	25 26	syl	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( ( 𝐴 ∪ 𝐵 ) ∈ HF ↔ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ω ) )
28	24 27	mpbird	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ HF )