disjpreima

Description: A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017)

		Ref	Expression
	Assertion	disjpreima	$⊢ (Fun F \land \underset{x \in A}{Disj} B) \to \underset{x \in A}{Disj} F^{-1} [B]$

Proof

Step	Hyp	Ref	Expression
1		inpreima	$⊢ Fun F \to F^{-1} [⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B] = F^{-1} [⦋ y / x ⦌ B] \cap F^{-1} [⦋ z / x ⦌ B]$
2		imaeq2	$⊢ ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset \to F^{-1} [⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B] = F^{-1} [\emptyset]$
3		ima0	$⊢ F^{-1} [\emptyset] = \emptyset$
4	2 3	eqtrdi	$⊢ ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset \to F^{-1} [⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B] = \emptyset$
5	1 4	sylan9req	$⊢ (Fun F \land ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset) \to F^{-1} [⦋ y / x ⦌ B] \cap F^{-1} [⦋ z / x ⦌ B] = \emptyset$
6	5	ex	$⊢ Fun F \to (⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset \to F^{-1} [⦋ y / x ⦌ B] \cap F^{-1} [⦋ z / x ⦌ B] = \emptyset)$
7		csbima12	$⊢ ⦋ y / x ⦌ F^{-1} [B] = ⦋ y / x ⦌ F^{-1} [⦋ y / x ⦌ B]$
8		csbconstg	$⊢ y \in V \to ⦋ y / x ⦌ F^{-1} = F^{-1}$
9	8	elv	$⊢ ⦋ y / x ⦌ F^{-1} = F^{-1}$
10	9	imaeq1i	$⊢ ⦋ y / x ⦌ F^{-1} [⦋ y / x ⦌ B] = F^{-1} [⦋ y / x ⦌ B]$
11	7 10	eqtri	$⊢ ⦋ y / x ⦌ F^{-1} [B] = F^{-1} [⦋ y / x ⦌ B]$
12		csbima12	$⊢ ⦋ z / x ⦌ F^{-1} [B] = ⦋ z / x ⦌ F^{-1} [⦋ z / x ⦌ B]$
13		csbconstg	$⊢ z \in V \to ⦋ z / x ⦌ F^{-1} = F^{-1}$
14	13	elv	$⊢ ⦋ z / x ⦌ F^{-1} = F^{-1}$
15	14	imaeq1i	$⊢ ⦋ z / x ⦌ F^{-1} [⦋ z / x ⦌ B] = F^{-1} [⦋ z / x ⦌ B]$
16	12 15	eqtri	$⊢ ⦋ z / x ⦌ F^{-1} [B] = F^{-1} [⦋ z / x ⦌ B]$
17	11 16	ineq12i	$⊢ ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = F^{-1} [⦋ y / x ⦌ B] \cap F^{-1} [⦋ z / x ⦌ B]$
18	17	eqeq1i	$⊢ ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset \leftrightarrow F^{-1} [⦋ y / x ⦌ B] \cap F^{-1} [⦋ z / x ⦌ B] = \emptyset$
19	6 18	imbitrrdi	$⊢ Fun F \to (⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset \to ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset)$
20	19	orim2d	$⊢ Fun F \to ((y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset) \to (y = z \lor ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset))$
21	20	ralimdv	$⊢ Fun F \to (\forall z \in A (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset) \to \forall z \in A (y = z \lor ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset))$
22	21	ralimdv	$⊢ Fun F \to (\forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset) \to \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset))$
23		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)$
24		disjors	$⊢ \underset{x \in A}{Disj} F^{-1} [B] \leftrightarrow \forall y \in A \forall z \in A (y = z \lor ⦋ y / x ⦌ F^{-1} [B] \cap ⦋ z / x ⦌ F^{-1} [B] = \emptyset)$
25	22 23 24	3imtr4g	$⊢ Fun F \to (\underset{x \in A}{Disj} B \to \underset{x \in A}{Disj} F^{-1} [B])$
26	25	imp	$⊢ (Fun F \land \underset{x \in A}{Disj} B) \to \underset{x \in A}{Disj} F^{-1} [B]$

Metamath Proof Explorer

Theorem disjpreima

Proof