firest

Description: The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	firest	$⊢ fi (J ↾_{𝑡} A) = fi (J) ↾_{𝑡} A$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ J ↾_{𝑡} A \in V$
2		elfi2	$⊢ J ↾_{𝑡} A \in V \to (x \in fi (J ↾_{𝑡} A) \leftrightarrow \exists y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\}) x = ⋂ y)$
3	1 2	ax-mp	$⊢ x \in fi (J ↾_{𝑡} A) \leftrightarrow \exists y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\}) x = ⋂ y$
4		eldifi	$⊢ y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\}) \to y \in (𝒫 (J ↾_{𝑡} A) \cap Fin)$
5	4	adantl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to y \in (𝒫 (J ↾_{𝑡} A) \cap Fin)$
6	5	elin2d	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to y \in Fin$
7		elfpw	$⊢ y \in (𝒫 (J ↾_{𝑡} A) \cap Fin) \leftrightarrow (y \subseteq J ↾_{𝑡} A \land y \in Fin)$
8	7	simplbi	$⊢ y \in (𝒫 (J ↾_{𝑡} A) \cap Fin) \to y \subseteq J ↾_{𝑡} A$
9	5 8	syl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to y \subseteq J ↾_{𝑡} A$
10	9	sseld	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to (z \in y \to z \in (J ↾_{𝑡} A))$
11		elrest	$⊢ (J \in V \land A \in V) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists y \in J z = y \cap A)$
12	11	adantr	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists y \in J z = y \cap A)$
13	10 12	sylibd	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to (z \in y \to \exists y \in J z = y \cap A)$
14	13	ralrimiv	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to \forall z \in y \exists y \in J z = y \cap A$
15		ineq1	$⊢ y = f (z) \to y \cap A = f (z) \cap A$
16	15	eqeq2d	$⊢ y = f (z) \to (z = y \cap A \leftrightarrow z = f (z) \cap A)$
17	16	ac6sfi	$⊢ (y \in Fin \land \forall z \in y \exists y \in J z = y \cap A) \to \exists f (f : y ⟶ J \land \forall z \in y z = f (z) \cap A)$
18	6 14 17	syl2anc	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to \exists f (f : y ⟶ J \land \forall z \in y z = f (z) \cap A)$
19		eldifsni	$⊢ y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\}) \to y \neq \emptyset$
20	19	ad2antlr	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to y \neq \emptyset$
21		iinin1	$⊢ y \neq \emptyset \to ⋂_{z \in y} (f (z) \cap A) = ⋂_{z \in y} f (z) \cap A$
22	20 21	syl	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂_{z \in y} (f (z) \cap A) = ⋂_{z \in y} f (z) \cap A$
23		fvex	$⊢ fi (J) \in V$
24		simpllr	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to A \in V$
25		ffn	$⊢ f : y ⟶ J \to f Fn y$
26	25	adantl	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to f Fn y$
27		fniinfv	$⊢ f Fn y \to ⋂_{z \in y} f (z) = ⋂ ran f$
28	26 27	syl	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂_{z \in y} f (z) = ⋂ ran f$
29		simplll	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to J \in V$
30		simpr	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to f : y ⟶ J$
31	6	adantr	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to y \in Fin$
32		intrnfi	$⊢ (J \in V \land (f : y ⟶ J \land y \neq \emptyset \land y \in Fin)) \to ⋂ ran f \in fi (J)$
33	29 30 20 31 32	syl13anc	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂ ran f \in fi (J)$
34	28 33	eqeltrd	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂_{z \in y} f (z) \in fi (J)$
35		elrestr	$⊢ (fi (J) \in V \land A \in V \land ⋂_{z \in y} f (z) \in fi (J)) \to ⋂_{z \in y} f (z) \cap A \in (fi (J) ↾_{𝑡} A)$
36	23 24 34 35	mp3an2i	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂_{z \in y} f (z) \cap A \in (fi (J) ↾_{𝑡} A)$
37	22 36	eqeltrd	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to ⋂_{z \in y} (f (z) \cap A) \in (fi (J) ↾_{𝑡} A)$
38		intiin	$⊢ ⋂ y = ⋂_{z \in y} z$
39		iineq2	$⊢ \forall z \in y z = f (z) \cap A \to ⋂_{z \in y} z = ⋂_{z \in y} (f (z) \cap A)$
40	38 39	syl5eq	$⊢ \forall z \in y z = f (z) \cap A \to ⋂ y = ⋂_{z \in y} (f (z) \cap A)$
41	40	eleq1d	$⊢ \forall z \in y z = f (z) \cap A \to (⋂ y \in (fi (J) ↾_{𝑡} A) \leftrightarrow ⋂_{z \in y} (f (z) \cap A) \in (fi (J) ↾_{𝑡} A))$
42	37 41	syl5ibrcom	$⊢ (((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \land f : y ⟶ J) \to (\forall z \in y z = f (z) \cap A \to ⋂ y \in (fi (J) ↾_{𝑡} A))$
43	42	expimpd	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to ((f : y ⟶ J \land \forall z \in y z = f (z) \cap A) \to ⋂ y \in (fi (J) ↾_{𝑡} A))$
44	43	exlimdv	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to (\exists f (f : y ⟶ J \land \forall z \in y z = f (z) \cap A) \to ⋂ y \in (fi (J) ↾_{𝑡} A))$
45	18 44	mpd	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to ⋂ y \in (fi (J) ↾_{𝑡} A)$
46		eleq1	$⊢ x = ⋂ y \to (x \in (fi (J) ↾_{𝑡} A) \leftrightarrow ⋂ y \in (fi (J) ↾_{𝑡} A))$
47	45 46	syl5ibrcom	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\})) \to (x = ⋂ y \to x \in (fi (J) ↾_{𝑡} A))$
48	47	rexlimdva	$⊢ (J \in V \land A \in V) \to (\exists y \in ((𝒫 (J ↾_{𝑡} A) \cap Fin) ∖ \{\emptyset\}) x = ⋂ y \to x \in (fi (J) ↾_{𝑡} A))$
49	3 48	syl5bi	$⊢ (J \in V \land A \in V) \to (x \in fi (J ↾_{𝑡} A) \to x \in (fi (J) ↾_{𝑡} A))$
50		simpr	$⊢ (J \in V \land A \in V) \to A \in V$
51		elrest	$⊢ (fi (J) \in V \land A \in V) \to (x \in (fi (J) ↾_{𝑡} A) \leftrightarrow \exists z \in fi (J) x = z \cap A)$
52	23 50 51	sylancr	$⊢ (J \in V \land A \in V) \to (x \in (fi (J) ↾_{𝑡} A) \leftrightarrow \exists z \in fi (J) x = z \cap A)$
53		elfi2	$⊢ J \in V \to (z \in fi (J) \leftrightarrow \exists y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\}) z = ⋂ y)$
54	53	adantr	$⊢ (J \in V \land A \in V) \to (z \in fi (J) \leftrightarrow \exists y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\}) z = ⋂ y)$
55		eldifsni	$⊢ y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\}) \to y \neq \emptyset$
56	55	adantl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to y \neq \emptyset$
57		iinin1	$⊢ y \neq \emptyset \to ⋂_{z \in y} (z \cap A) = ⋂_{z \in y} z \cap A$
58	56 57	syl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to ⋂_{z \in y} (z \cap A) = ⋂_{z \in y} z \cap A$
59	38	ineq1i	$⊢ ⋂ y \cap A = ⋂_{z \in y} z \cap A$
60	58 59	eqtr4di	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to ⋂_{z \in y} (z \cap A) = ⋂ y \cap A$
61		ovexd	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to J ↾_{𝑡} A \in V$
62		eldifi	$⊢ y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\}) \to y \in (𝒫 J \cap Fin)$
63	62	adantl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to y \in (𝒫 J \cap Fin)$
64		elfpw	$⊢ y \in (𝒫 J \cap Fin) \leftrightarrow (y \subseteq J \land y \in Fin)$
65	64	simplbi	$⊢ y \in (𝒫 J \cap Fin) \to y \subseteq J$
66	63 65	syl	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to y \subseteq J$
67		elrestr	$⊢ (J \in V \land A \in V \land z \in J) \to z \cap A \in (J ↾_{𝑡} A)$
68	67	3expa	$⊢ ((J \in V \land A \in V) \land z \in J) \to z \cap A \in (J ↾_{𝑡} A)$
69	68	ralrimiva	$⊢ (J \in V \land A \in V) \to \forall z \in J z \cap A \in (J ↾_{𝑡} A)$
70	69	adantr	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to \forall z \in J z \cap A \in (J ↾_{𝑡} A)$
71		ssralv	$⊢ y \subseteq J \to (\forall z \in J z \cap A \in (J ↾_{𝑡} A) \to \forall z \in y z \cap A \in (J ↾_{𝑡} A))$
72	66 70 71	sylc	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to \forall z \in y z \cap A \in (J ↾_{𝑡} A)$
73	63	elin2d	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to y \in Fin$
74		iinfi	$⊢ (J ↾_{𝑡} A \in V \land (\forall z \in y z \cap A \in (J ↾_{𝑡} A) \land y \neq \emptyset \land y \in Fin)) \to ⋂_{z \in y} (z \cap A) \in fi (J ↾_{𝑡} A)$
75	61 72 56 73 74	syl13anc	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to ⋂_{z \in y} (z \cap A) \in fi (J ↾_{𝑡} A)$
76	60 75	eqeltrrd	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to ⋂ y \cap A \in fi (J ↾_{𝑡} A)$
77		eleq1	$⊢ x = ⋂ y \cap A \to (x \in fi (J ↾_{𝑡} A) \leftrightarrow ⋂ y \cap A \in fi (J ↾_{𝑡} A))$
78	76 77	syl5ibrcom	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to (x = ⋂ y \cap A \to x \in fi (J ↾_{𝑡} A))$
79		ineq1	$⊢ z = ⋂ y \to z \cap A = ⋂ y \cap A$
80	79	eqeq2d	$⊢ z = ⋂ y \to (x = z \cap A \leftrightarrow x = ⋂ y \cap A)$
81	80	imbi1d	$⊢ z = ⋂ y \to ((x = z \cap A \to x \in fi (J ↾_{𝑡} A)) \leftrightarrow (x = ⋂ y \cap A \to x \in fi (J ↾_{𝑡} A)))$
82	78 81	syl5ibrcom	$⊢ ((J \in V \land A \in V) \land y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\})) \to (z = ⋂ y \to (x = z \cap A \to x \in fi (J ↾_{𝑡} A)))$
83	82	rexlimdva	$⊢ (J \in V \land A \in V) \to (\exists y \in ((𝒫 J \cap Fin) ∖ \{\emptyset\}) z = ⋂ y \to (x = z \cap A \to x \in fi (J ↾_{𝑡} A)))$
84	54 83	sylbid	$⊢ (J \in V \land A \in V) \to (z \in fi (J) \to (x = z \cap A \to x \in fi (J ↾_{𝑡} A)))$
85	84	rexlimdv	$⊢ (J \in V \land A \in V) \to (\exists z \in fi (J) x = z \cap A \to x \in fi (J ↾_{𝑡} A))$
86	52 85	sylbid	$⊢ (J \in V \land A \in V) \to (x \in (fi (J) ↾_{𝑡} A) \to x \in fi (J ↾_{𝑡} A))$
87	49 86	impbid	$⊢ (J \in V \land A \in V) \to (x \in fi (J ↾_{𝑡} A) \leftrightarrow x \in (fi (J) ↾_{𝑡} A))$
88	87	eqrdv	$⊢ (J \in V \land A \in V) \to fi (J ↾_{𝑡} A) = fi (J) ↾_{𝑡} A$
89		fi0	$⊢ fi (\emptyset) = \emptyset$
90		relxp	$⊢ Rel (V \times V)$
91		restfn	$⊢ ↾_{𝑡} Fn (V \times V)$
92	91	fndmi	$⊢ dom ↾_{𝑡} = V \times V$
93	92	releqi	$⊢ Rel dom ↾_{𝑡} \leftrightarrow Rel (V \times V)$
94	90 93	mpbir	$⊢ Rel dom ↾_{𝑡}$
95	94	ovprc	$⊢ \neg (J \in V \land A \in V) \to J ↾_{𝑡} A = \emptyset$
96	95	fveq2d	$⊢ \neg (J \in V \land A \in V) \to fi (J ↾_{𝑡} A) = fi (\emptyset)$
97		ianor	$⊢ \neg (J \in V \land A \in V) \leftrightarrow (\neg J \in V \lor \neg A \in V)$
98		fvprc	$⊢ \neg J \in V \to fi (J) = \emptyset$
99	98	oveq1d	$⊢ \neg J \in V \to fi (J) ↾_{𝑡} A = \emptyset ↾_{𝑡} A$
100		0rest	$⊢ \emptyset ↾_{𝑡} A = \emptyset$
101	99 100	eqtrdi	$⊢ \neg J \in V \to fi (J) ↾_{𝑡} A = \emptyset$
102	94	ovprc2	$⊢ \neg A \in V \to fi (J) ↾_{𝑡} A = \emptyset$
103	101 102	jaoi	$⊢ (\neg J \in V \lor \neg A \in V) \to fi (J) ↾_{𝑡} A = \emptyset$
104	97 103	sylbi	$⊢ \neg (J \in V \land A \in V) \to fi (J) ↾_{𝑡} A = \emptyset$
105	89 96 104	3eqtr4a	$⊢ \neg (J \in V \land A \in V) \to fi (J ↾_{𝑡} A) = fi (J) ↾_{𝑡} A$
106	88 105	pm2.61i	$⊢ fi (J ↾_{𝑡} A) = fi (J) ↾_{𝑡} A$

Metamath Proof Explorer

Theorem firest

Proof