disjxp1

Description: The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypothesis	disjxp1.1	$⊢ φ \to \underset{x \in A}{Disj} B$
	Assertion	disjxp1	$⊢ φ \to \underset{x \in A}{Disj} (B \times C)$

Proof

Step	Hyp	Ref	Expression
1		disjxp1.1	$⊢ φ \to \underset{x \in A}{Disj} B$
2		animorrl	$⊢ ((φ \land (y \in A \land z \in A)) \land y = z) \to (y = z \lor ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset)$
3		csbxp	$⊢ ⦋ y / x ⦌ (B \times C) = ⦋ y / x ⦌ B \times ⦋ y / x ⦌ C$
4		csbxp	$⊢ ⦋ z / x ⦌ (B \times C) = ⦋ z / x ⦌ B \times ⦋ z / x ⦌ C$
5	3 4	ineq12i	$⊢ ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = (⦋ y / x ⦌ B \times ⦋ y / x ⦌ C) \cap (⦋ z / x ⦌ B \times ⦋ z / x ⦌ C)$
6		simpll	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to φ$
7		simplrl	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to y \in A$
8		simplrr	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to z \in A$
9	6 7 8	jca31	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to ((φ \land y \in A) \land z \in A)$
10		simpr	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to y \neq z$
11	10	neneqd	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to \neg y = z$
12		disjors	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset)$
13	1 12	sylib	$⊢ φ \to \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset)$
14	13	r19.21bi	$⊢ (φ \land y \in A) \to \forall z \in A (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset)$
15	14	r19.21bi	$⊢ ((φ \land y \in A) \land z \in A) \to (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset)$
16	15	ord	$⊢ ((φ \land y \in A) \land z \in A) \to (\neg y = z \to ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset)$
17	9 11 16	sylc	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset$
18		xpdisj1	$⊢ ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset \to (⦋ y / x ⦌ B \times ⦋ y / x ⦌ C) \cap (⦋ z / x ⦌ B \times ⦋ z / x ⦌ C) = \emptyset$
19	17 18	syl	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to (⦋ y / x ⦌ B \times ⦋ y / x ⦌ C) \cap (⦋ z / x ⦌ B \times ⦋ z / x ⦌ C) = \emptyset$
20	5 19	syl5eq	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset$
21	20	olcd	$⊢ ((φ \land (y \in A \land z \in A)) \land y \neq z) \to (y = z \lor ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset)$
22	2 21	pm2.61dane	$⊢ (φ \land (y \in A \land z \in A)) \to (y = z \lor ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset)$
23	22	ralrimivva	$⊢ φ \to \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset)$
24		disjors	$⊢ \underset{x \in A}{Disj} (B \times C) \leftrightarrow \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ (B \times C) \cap ⦋ z / x ⦌ (B \times C) = \emptyset)$
25	23 24	sylibr	$⊢ φ \to \underset{x \in A}{Disj} (B \times C)$

Metamath Proof Explorer

Theorem disjxp1

Proof