fun11uni

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004)

		Ref	Expression
	Assertion	fun11uni	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (Fun ⋃ A \land Fun {⋃ A}^{-1})$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (Fun f \land Fun f^{-1}) \to Fun f$
2	1	anim1i	$⊢ ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f))$
3	2	ralimi	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f))$
4		fununi	$⊢ \forall f \in A (Fun f \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun ⋃ A$
5	3 4	syl	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun ⋃ A$
6		simpr	$⊢ (Fun f \land Fun f^{-1}) \to Fun f^{-1}$
7	6	anim1i	$⊢ ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f))$
8	7	ralimi	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f))$
9		funcnvuni	$⊢ \forall f \in A (Fun f^{-1} \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun {⋃ A}^{-1}$
10	8 9	syl	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to Fun {⋃ A}^{-1}$
11	5 10	jca	$⊢ \forall f \in A ((Fun f \land Fun f^{-1}) \land \forall g \in A (f \subseteq g \lor g \subseteq f)) \to (Fun ⋃ A \land Fun {⋃ A}^{-1})$

Metamath Proof Explorer