restfpw

Description: The restriction of the set of finite subsets of A is the set of finite subsets of B . (Contributed by Mario Carneiro, 18-Sep-2015)

		Ref	Expression
	Assertion	restfpw	$⊢ (A \in V \land B \subseteq A) \to (𝒫 A \cap Fin) ↾_{𝑡} B = 𝒫 B \cap Fin$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$⊢ A \in V \to 𝒫 A \in V$
2	1	adantr	$⊢ (A \in V \land B \subseteq A) \to 𝒫 A \in V$
3		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
4	2 3	syl	$⊢ (A \in V \land B \subseteq A) \to 𝒫 A \cap Fin \in V$
5		ssexg	$⊢ (B \subseteq A \land A \in V) \to B \in V$
6	5	ancoms	$⊢ (A \in V \land B \subseteq A) \to B \in V$
7		restval	$⊢ (𝒫 A \cap Fin \in V \land B \in V) \to (𝒫 A \cap Fin) ↾_{𝑡} B = ran (x \in (𝒫 A \cap Fin) ⟼ x \cap B)$
8	4 6 7	syl2anc	$⊢ (A \in V \land B \subseteq A) \to (𝒫 A \cap Fin) ↾_{𝑡} B = ran (x \in (𝒫 A \cap Fin) ⟼ x \cap B)$
9		inss2	$⊢ x \cap B \subseteq B$
10	9	a1i	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 A \cap Fin)) \to x \cap B \subseteq B$
11		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
12	11	adantl	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
13		inss1	$⊢ x \cap B \subseteq x$
14		ssfi	$⊢ (x \in Fin \land x \cap B \subseteq x) \to x \cap B \in Fin$
15	12 13 14	sylancl	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 A \cap Fin)) \to x \cap B \in Fin$
16		elfpw	$⊢ x \cap B \in (𝒫 B \cap Fin) \leftrightarrow (x \cap B \subseteq B \land x \cap B \in Fin)$
17	10 15 16	sylanbrc	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 A \cap Fin)) \to x \cap B \in (𝒫 B \cap Fin)$
18	17	fmpttd	$⊢ (A \in V \land B \subseteq A) \to (x \in (𝒫 A \cap Fin) ⟼ x \cap B) : 𝒫 A \cap Fin ⟶ 𝒫 B \cap Fin$
19	18	frnd	$⊢ (A \in V \land B \subseteq A) \to ran (x \in (𝒫 A \cap Fin) ⟼ x \cap B) \subseteq 𝒫 B \cap Fin$
20	8 19	eqsstrd	$⊢ (A \in V \land B \subseteq A) \to (𝒫 A \cap Fin) ↾_{𝑡} B \subseteq 𝒫 B \cap Fin$
21		elfpw	$⊢ x \in (𝒫 B \cap Fin) \leftrightarrow (x \subseteq B \land x \in Fin)$
22	21	simplbi	$⊢ x \in (𝒫 B \cap Fin) \to x \subseteq B$
23	22	adantl	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \subseteq B$
24		dfss2	$⊢ x \subseteq B \leftrightarrow x \cap B = x$
25	23 24	sylib	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \cap B = x$
26	4	adantr	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to 𝒫 A \cap Fin \in V$
27	6	adantr	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to B \in V$
28		simplr	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to B \subseteq A$
29	23 28	sstrd	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \subseteq A$
30		elinel2	$⊢ x \in (𝒫 B \cap Fin) \to x \in Fin$
31	30	adantl	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \in Fin$
32		elfpw	$⊢ x \in (𝒫 A \cap Fin) \leftrightarrow (x \subseteq A \land x \in Fin)$
33	29 31 32	sylanbrc	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \in (𝒫 A \cap Fin)$
34		elrestr	$⊢ (𝒫 A \cap Fin \in V \land B \in V \land x \in (𝒫 A \cap Fin)) \to x \cap B \in ((𝒫 A \cap Fin) ↾_{𝑡} B)$
35	26 27 33 34	syl3anc	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \cap B \in ((𝒫 A \cap Fin) ↾_{𝑡} B)$
36	25 35	eqeltrrd	$⊢ ((A \in V \land B \subseteq A) \land x \in (𝒫 B \cap Fin)) \to x \in ((𝒫 A \cap Fin) ↾_{𝑡} B)$
37	20 36	eqelssd	$⊢ (A \in V \land B \subseteq A) \to (𝒫 A \cap Fin) ↾_{𝑡} B = 𝒫 B \cap Fin$

Metamath Proof Explorer

Theorem restfpw

Proof