Metamath Proof Explorer

Theorem unen

Description: Equinumerosity of union of disjoint sets. Theorem 4 of Suppes p. 92. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	unen	$⊢ ((A \approx B \land C \approx D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (A \cup C) \approx (B \cup D)$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists x x : A \underset{1-1 onto}{⟶} B$
2		bren	$⊢ C \approx D \leftrightarrow \exists y y : C \underset{1-1 onto}{⟶} D$
3		exdistrv	$⊢ \exists x \exists y (x : A \underset{1-1 onto}{⟶} B \land y : C \underset{1-1 onto}{⟶} D) \leftrightarrow (\exists x x : A \underset{1-1 onto}{⟶} B \land \exists y y : C \underset{1-1 onto}{⟶} D)$
4		vex	$⊢ x \in V$
5		vex	$⊢ y \in V$
6	4 5	unex	$⊢ x \cup y \in V$
7		f1oun	$⊢ ((x : A \underset{1-1 onto}{⟶} B \land y : C \underset{1-1 onto}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (x \cup y) : A \cup C \underset{1-1 onto}{⟶} B \cup D$
8		f1oen3g	$⊢ (x \cup y \in V \land (x \cup y) : A \cup C \underset{1-1 onto}{⟶} B \cup D) \to (A \cup C) \approx (B \cup D)$
9	6 7 8	sylancr	$⊢ ((x : A \underset{1-1 onto}{⟶} B \land y : C \underset{1-1 onto}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (A \cup C) \approx (B \cup D)$
10	9	ex	$⊢ (x : A \underset{1-1 onto}{⟶} B \land y : C \underset{1-1 onto}{⟶} D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to (A \cup C) \approx (B \cup D))$
11	10	exlimivv	$⊢ \exists x \exists y (x : A \underset{1-1 onto}{⟶} B \land y : C \underset{1-1 onto}{⟶} D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to (A \cup C) \approx (B \cup D))$
12	3 11	sylbir	$⊢ (\exists x x : A \underset{1-1 onto}{⟶} B \land \exists y y : C \underset{1-1 onto}{⟶} D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to (A \cup C) \approx (B \cup D))$
13	1 2 12	syl2anb	$⊢ (A \approx B \land C \approx D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to (A \cup C) \approx (B \cup D))$
14	13	imp	$⊢ ((A \approx B \land C \approx D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (A \cup C) \approx (B \cup D)$