disjss3

Description: Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016)

		Ref	Expression
	Assertion	disjss3	$⊢ (A \subseteq B \land \forall x \in (B ∖ A) C = \emptyset) \to (\underset{x \in A}{Disj} C \leftrightarrow \underset{x \in B}{Disj} C)$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall x \in (B ∖ A) C = \emptyset \leftrightarrow \forall x (x \in (B ∖ A) \to C = \emptyset)$
2		simprr	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to y \in C$
3		n0i	$⊢ y \in C \to \neg C = \emptyset$
4	2 3	syl	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to \neg C = \emptyset$
5		simpl	$⊢ (x \in B \land y \in C) \to x \in B$
6	5	adantl	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to x \in B$
7		eldif	$⊢ x \in (B ∖ A) \leftrightarrow (x \in B \land \neg x \in A)$
8		simpl	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to (x \in (B ∖ A) \to C = \emptyset)$
9	7 8	syl5bir	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to ((x \in B \land \neg x \in A) \to C = \emptyset)$
10	6 9	mpand	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to (\neg x \in A \to C = \emptyset)$
11	4 10	mt3d	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to x \in A$
12	11 2	jca	$⊢ ((x \in (B ∖ A) \to C = \emptyset) \land (x \in B \land y \in C)) \to (x \in A \land y \in C)$
13	12	ex	$⊢ (x \in (B ∖ A) \to C = \emptyset) \to ((x \in B \land y \in C) \to (x \in A \land y \in C))$
14	13	alimi	$⊢ \forall x (x \in (B ∖ A) \to C = \emptyset) \to \forall x ((x \in B \land y \in C) \to (x \in A \land y \in C))$
15	1 14	sylbi	$⊢ \forall x \in (B ∖ A) C = \emptyset \to \forall x ((x \in B \land y \in C) \to (x \in A \land y \in C))$
16		moim	$⊢ \forall x ((x \in B \land y \in C) \to (x \in A \land y \in C)) \to (\exists^{} x (x \in A \land y \in C) \to \exists^{} x (x \in B \land y \in C))$
17	15 16	syl	$⊢ \forall x \in (B ∖ A) C = \emptyset \to (\exists^{} x (x \in A \land y \in C) \to \exists^{} x (x \in B \land y \in C))$
18	17	alimdv	$⊢ \forall x \in (B ∖ A) C = \emptyset \to (\forall y \exists^{} x (x \in A \land y \in C) \to \forall y \exists^{} x (x \in B \land y \in C))$
19		dfdisj2	$⊢ \underset{x \in A}{Disj} C \leftrightarrow \forall y \exists^{*} x (x \in A \land y \in C)$
20		dfdisj2	$⊢ \underset{x \in B}{Disj} C \leftrightarrow \forall y \exists^{*} x (x \in B \land y \in C)$
21	18 19 20	3imtr4g	$⊢ \forall x \in (B ∖ A) C = \emptyset \to (\underset{x \in A}{Disj} C \to \underset{x \in B}{Disj} C)$
22	21	adantl	$⊢ (A \subseteq B \land \forall x \in (B ∖ A) C = \emptyset) \to (\underset{x \in A}{Disj} C \to \underset{x \in B}{Disj} C)$
23		disjss1	$⊢ A \subseteq B \to (\underset{x \in B}{Disj} C \to \underset{x \in A}{Disj} C)$
24	23	adantr	$⊢ (A \subseteq B \land \forall x \in (B ∖ A) C = \emptyset) \to (\underset{x \in B}{Disj} C \to \underset{x \in A}{Disj} C)$
25	22 24	impbid	$⊢ (A \subseteq B \land \forall x \in (B ∖ A) C = \emptyset) \to (\underset{x \in A}{Disj} C \leftrightarrow \underset{x \in B}{Disj} C)$

Metamath Proof Explorer

Theorem disjss3

Proof