hfun

Description: The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015)

		Ref	Expression
	Assertion	hfun	$⊢ (A \in Hf \land B \in Hf) \to A \cup B \in Hf$

Proof

Step	Hyp	Ref	Expression
1		rankung	$⊢ (A \in Hf \land B \in Hf) \to rank (A \cup B) = rank (A) \cup rank (B)$
2		elhf2g	$⊢ A \in Hf \to (A \in Hf \leftrightarrow rank (A) \in ω)$
3	2	ibi	$⊢ A \in Hf \to rank (A) \in ω$
4		elhf2g	$⊢ B \in Hf \to (B \in Hf \leftrightarrow rank (B) \in ω)$
5	4	ibi	$⊢ B \in Hf \to rank (B) \in ω$
6		eleq1a	$⊢ rank (B) \in ω \to (rank (A) \cup rank (B) = rank (B) \to rank (A) \cup rank (B) \in ω)$
7	6	adantl	$⊢ (rank (A) \in ω \land rank (B) \in ω) \to (rank (A) \cup rank (B) = rank (B) \to rank (A) \cup rank (B) \in ω)$
8		uncom	$⊢ rank (B) \cup rank (A) = rank (A) \cup rank (B)$
9	8	eqeq1i	$⊢ rank (B) \cup rank (A) = rank (A) \leftrightarrow rank (A) \cup rank (B) = rank (A)$
10	9	biimpi	$⊢ rank (B) \cup rank (A) = rank (A) \to rank (A) \cup rank (B) = rank (A)$
11	10	eleq1d	$⊢ rank (B) \cup rank (A) = rank (A) \to (rank (A) \cup rank (B) \in ω \leftrightarrow rank (A) \in ω)$
12	11	biimprcd	$⊢ rank (A) \in ω \to (rank (B) \cup rank (A) = rank (A) \to rank (A) \cup rank (B) \in ω)$
13	12	adantr	$⊢ (rank (A) \in ω \land rank (B) \in ω) \to (rank (B) \cup rank (A) = rank (A) \to rank (A) \cup rank (B) \in ω)$
14		nnord	$⊢ rank (A) \in ω \to Ord rank (A)$
15		nnord	$⊢ rank (B) \in ω \to Ord rank (B)$
16		ordtri2or2	$⊢ (Ord rank (A) \land Ord rank (B)) \to (rank (A) \subseteq rank (B) \lor rank (B) \subseteq rank (A))$
17	14 15 16	syl2an	$⊢ (rank (A) \in ω \land rank (B) \in ω) \to (rank (A) \subseteq rank (B) \lor rank (B) \subseteq rank (A))$
18		ssequn1	$⊢ rank (A) \subseteq rank (B) \leftrightarrow rank (A) \cup rank (B) = rank (B)$
19		ssequn1	$⊢ rank (B) \subseteq rank (A) \leftrightarrow rank (B) \cup rank (A) = rank (A)$
20	18 19	orbi12i	$⊢ (rank (A) \subseteq rank (B) \lor rank (B) \subseteq rank (A)) \leftrightarrow (rank (A) \cup rank (B) = rank (B) \lor rank (B) \cup rank (A) = rank (A))$
21	17 20	sylib	$⊢ (rank (A) \in ω \land rank (B) \in ω) \to (rank (A) \cup rank (B) = rank (B) \lor rank (B) \cup rank (A) = rank (A))$
22	7 13 21	mpjaod	$⊢ (rank (A) \in ω \land rank (B) \in ω) \to rank (A) \cup rank (B) \in ω$
23	3 5 22	syl2an	$⊢ (A \in Hf \land B \in Hf) \to rank (A) \cup rank (B) \in ω$
24	1 23	eqeltrd	$⊢ (A \in Hf \land B \in Hf) \to rank (A \cup B) \in ω$
25		unexg	$⊢ (A \in Hf \land B \in Hf) \to A \cup B \in V$
26		elhf2g	$⊢ A \cup B \in V \to (A \cup B \in Hf \leftrightarrow rank (A \cup B) \in ω)$
27	25 26	syl	$⊢ (A \in Hf \land B \in Hf) \to (A \cup B \in Hf \leftrightarrow rank (A \cup B) \in ω)$
28	24 27	mpbird	$⊢ (A \in Hf \land B \in Hf) \to A \cup B \in Hf$

Metamath Proof Explorer

Theorem hfun

Proof