2ndpreima

Description: The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017)

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

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	anbi1i	$⊢ (w \in (B \times C) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)) \land 2^{nd} (w) \in A)$
3		ssel	$⊢ A \subseteq C \to (2^{nd} (w) \in A \to 2^{nd} (w) \in C)$
4	3	pm4.71rd	$⊢ A \subseteq C \to (2^{nd} (w) \in A \leftrightarrow (2^{nd} (w) \in C \land 2^{nd} (w) \in A))$
5	4	anbi2d	$⊢ A \subseteq C \to (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land 1^{st} (w) \in B) \land (2^{nd} (w) \in C \land 2^{nd} (w) \in A)))$
6		anass	$⊢ (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land 1^{st} (w) \in B) \land (2^{nd} (w) \in C \land 2^{nd} (w) \in A))$
7	6	bicomi	$⊢ ((w \in (V \times V) \land 1^{st} (w) \in B) \land (2^{nd} (w) \in C \land 2^{nd} (w) \in A)) \leftrightarrow (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \land 2^{nd} (w) \in A)$
8	7	a1i	$⊢ A \subseteq C \to (((w \in (V \times V) \land 1^{st} (w) \in B) \land (2^{nd} (w) \in C \land 2^{nd} (w) \in A)) \leftrightarrow (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \land 2^{nd} (w) \in A))$
9		anass	$⊢ ((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C))$
10	9	anbi1i	$⊢ (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)) \land 2^{nd} (w) \in A)$
11	10	a1i	$⊢ A \subseteq C \to ((((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in C) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)) \land 2^{nd} (w) \in A))$
12	5 8 11	3bitrd	$⊢ A \subseteq C \to (((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in C)) \land 2^{nd} (w) \in A))$
13	2 12	bitr4id	$⊢ A \subseteq C \to ((w \in (B \times C) \land 2^{nd} (w) \in A) \leftrightarrow ((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in A))$
14		ancom	$⊢ (w \in (B \times C) \land 2^{nd} (w) \in A) \leftrightarrow (2^{nd} (w) \in A \land w \in (B \times C))$
15		anass	$⊢ ((w \in (V \times V) \land 1^{st} (w) \in B) \land 2^{nd} (w) \in A) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in A))$
16	13 14 15	3bitr3g	$⊢ A \subseteq C \to ((2^{nd} (w) \in A \land w \in (B \times C)) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in A)))$
17		cnvresima	$⊢ {({2^{nd} ↾}_{(B \times C)})}^{-1} [A] = {2^{nd}}^{-1} [A] \cap (B \times C)$
18	17	eleq2i	$⊢ w \in {({2^{nd} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow w \in ({2^{nd}}^{-1} [A] \cap (B \times C))$
19		elin	$⊢ w \in ({2^{nd}}^{-1} [A] \cap (B \times C)) \leftrightarrow (w \in {2^{nd}}^{-1} [A] \land w \in (B \times C))$
20		vex	$⊢ w \in V$
21		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
22		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
23		elpreima	$⊢ 2^{nd} Fn V \to (w \in {2^{nd}}^{-1} [A] \leftrightarrow (w \in V \land 2^{nd} (w) \in A))$
24	21 22 23	mp2b	$⊢ w \in {2^{nd}}^{-1} [A] \leftrightarrow (w \in V \land 2^{nd} (w) \in A)$
25	20 24	mpbiran	$⊢ w \in {2^{nd}}^{-1} [A] \leftrightarrow 2^{nd} (w) \in A$
26	25	anbi1i	$⊢ (w \in {2^{nd}}^{-1} [A] \land w \in (B \times C)) \leftrightarrow (2^{nd} (w) \in A \land w \in (B \times C))$
27	18 19 26	3bitri	$⊢ w \in {({2^{nd} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow (2^{nd} (w) \in A \land w \in (B \times C))$
28		elxp7	$⊢ w \in (B \times A) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in B \land 2^{nd} (w) \in A))$
29	16 27 28	3bitr4g	$⊢ A \subseteq C \to (w \in {({2^{nd} ↾}_{(B \times C)})}^{-1} [A] \leftrightarrow w \in (B \times A))$
30	29	eqrdv	$⊢ A \subseteq C \to {({2^{nd} ↾}_{(B \times C)})}^{-1} [A] = B \times A$

Metamath Proof Explorer

Theorem 2ndpreima

Proof