1stpreima

Description: The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017)

		Ref	Expression
	Assertion	1stpreima	$⊢ A \subseteq B \to {({1^{st} ↾}_{(B \times C)})}^{-1} [A] = A \times C$

Proof

Step	Hyp	Ref	Expression
1		elxp7	$⊢ w \in (B \times C) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C))$
2	1	anbi2i	$⊢ (1^{st} (w) \in A \land w \in (B \times C)) \leftrightarrow (1^{st} (w) \in A \land (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)))$
3		anass	$⊢ ((1^{st} (w) \in A \land 1^{st} (w) \in B) \land (w \in (V \times V) \land 2^{nd} (w) \in C)) \leftrightarrow (1^{st} (w) \in A \land (1^{st} (w) \in B \land (w \in (V \times V) \land 2^{nd} (w) \in C)))$
4	3	a1i	$⊢ A \subseteq B \to (((1^{st} (w) \in A \land 1^{st} (w) \in B) \land (w \in (V \times V) \land 2^{nd} (w) \in C)) \leftrightarrow (1^{st} (w) \in A \land (1^{st} (w) \in B \land (w \in (V \times V) \land 2^{nd} (w) \in C))))$
5		ssel	$⊢ A \subseteq B \to (1^{st} (w) \in A \to 1^{st} (w) \in B)$
6	5	pm4.71d	$⊢ A \subseteq B \to (1^{st} (w) \in A \leftrightarrow (1^{st} (w) \in A \land 1^{st} (w) \in B))$
7	6	anbi1d	$⊢ A \subseteq B \to ((1^{st} (w) \in A \land (w \in (V \times V) \land 2^{nd} (w) \in C)) \leftrightarrow ((1^{st} (w) \in A \land 1^{st} (w) \in B) \land (w \in (V \times V) \land 2^{nd} (w) \in C)))$
8		an12	$⊢ (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)) \leftrightarrow (1^{st} (w) \in B \land (w \in (V \times V) \land 2^{nd} (w) \in C))$
9	8	anbi2i	$⊢ (1^{st} (w) \in A \land (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C))) \leftrightarrow (1^{st} (w) \in A \land (1^{st} (w) \in B \land (w \in (V \times V) \land 2^{nd} (w) \in C)))$
10	9	a1i	$⊢ A \subseteq B \to ((1^{st} (w) \in A \land (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C))) \leftrightarrow (1^{st} (w) \in A \land (1^{st} (w) \in B \land (w \in (V \times V) \land 2^{nd} (w) \in C))))$
11	4 7 10	3bitr4d	$⊢ A \subseteq B \to ((1^{st} (w) \in A \land (w \in (V \times V) \land 2^{nd} (w) \in C)) \leftrightarrow (1^{st} (w) \in A \land (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C))))$
12	2 11	bitr4id	$⊢ A \subseteq B \to ((1^{st} (w) \in A \land w \in (B \times C)) \leftrightarrow (1^{st} (w) \in A \land (w \in (V \times V) \land 2^{nd} (w) \in C)))$
13		an12	$⊢ (1^{st} (w) \in A \land (w \in (V \times V) \land 2^{nd} (w) \in C)) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in A \land 2^{nd} (w) \in C))$
14	12 13	bitrdi	$⊢ A \subseteq B \to ((1^{st} (w) \in A \land w \in (B \times C)) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in A \land 2^{nd} (w) \in C)))$
15		cnvresima	$⊢ {({1^{st} ↾}_{(B \times C)})}^{-1} [A] = {1^{st}}^{-1} [A] \cap (B \times C)$
16	15	eleq2i	$⊢ w \in {({1^{st} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow w \in ({1^{st}}^{-1} [A] \cap (B \times C))$
17		elin	$⊢ w \in ({1^{st}}^{-1} [A] \cap (B \times C)) \leftrightarrow (w \in {1^{st}}^{-1} [A] \land w \in (B \times C))$
18		vex	$⊢ w \in V$
19		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
20		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
21		elpreima	$⊢ 1^{st} Fn V \to (w \in {1^{st}}^{-1} [A] \leftrightarrow (w \in V \land 1^{st} (w) \in A))$
22	19 20 21	mp2b	$⊢ w \in {1^{st}}^{-1} [A] \leftrightarrow (w \in V \land 1^{st} (w) \in A)$
23	18 22	mpbiran	$⊢ w \in {1^{st}}^{-1} [A] \leftrightarrow 1^{st} (w) \in A$
24	23	anbi1i	$⊢ (w \in {1^{st}}^{-1} [A] \land w \in (B \times C)) \leftrightarrow (1^{st} (w) \in A \land w \in (B \times C))$
25	16 17 24	3bitri	$⊢ w \in {({1^{st} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow (1^{st} (w) \in A \land w \in (B \times C))$
26		elxp7	$⊢ w \in (A \times C) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in A \land 2^{nd} (w) \in C))$
27	14 25 26	3bitr4g	$⊢ A \subseteq B \to (w \in {({1^{st} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow w \in (A \times C))$
28	27	eqrdv	$⊢ A \subseteq B \to {({1^{st} ↾}_{(B \times C)})}^{-1} [A] = A \times C$

Metamath Proof Explorer

Theorem 1stpreima

Proof