elrfirn

Description: Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Assertion	elrfirn	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (A \in fi (\{B\} \cup ran F) \leftrightarrow \exists v \in (𝒫 I \cap Fin) A = B \cap ⋂_{y \in v} F (y))$

Proof

Step	Hyp	Ref	Expression
1		frn	$⊢ F : I ⟶ 𝒫 B \to ran F \subseteq 𝒫 B$
2		elrfi	$⊢ (B \in V \land ran F \subseteq 𝒫 B) \to (A \in fi (\{B\} \cup ran F) \leftrightarrow \exists w \in (𝒫 ran F \cap Fin) A = B \cap ⋂ w)$
3	1 2	sylan2	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (A \in fi (\{B\} \cup ran F) \leftrightarrow \exists w \in (𝒫 ran F \cap Fin) A = B \cap ⋂ w)$
4		imassrn	$⊢ F [v] \subseteq ran F$
5		pwexg	$⊢ B \in V \to 𝒫 B \in V$
6		ssexg	$⊢ (ran F \subseteq 𝒫 B \land 𝒫 B \in V) \to ran F \in V$
7	1 5 6	syl2anr	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to ran F \in V$
8		elpw2g	$⊢ ran F \in V \to (F [v] \in 𝒫 ran F \leftrightarrow F [v] \subseteq ran F)$
9	7 8	syl	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (F [v] \in 𝒫 ran F \leftrightarrow F [v] \subseteq ran F)$
10	4 9	mpbiri	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to F [v] \in 𝒫 ran F$
11	10	adantr	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to F [v] \in 𝒫 ran F$
12		ffun	$⊢ F : I ⟶ 𝒫 B \to Fun F$
13	12	ad2antlr	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to Fun F$
14		inss2	$⊢ 𝒫 I \cap Fin \subseteq Fin$
15	14	sseli	$⊢ v \in (𝒫 I \cap Fin) \to v \in Fin$
16	15	adantl	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to v \in Fin$
17		imafi	$⊢ (Fun F \land v \in Fin) \to F [v] \in Fin$
18	13 16 17	syl2anc	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to F [v] \in Fin$
19	11 18	elind	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to F [v] \in (𝒫 ran F \cap Fin)$
20		ffn	$⊢ F : I ⟶ 𝒫 B \to F Fn I$
21	20	ad2antlr	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w \in (𝒫 ran F \cap Fin)) \to F Fn I$
22		inss1	$⊢ 𝒫 ran F \cap Fin \subseteq 𝒫 ran F$
23	22	sseli	$⊢ w \in (𝒫 ran F \cap Fin) \to w \in 𝒫 ran F$
24	23	elpwid	$⊢ w \in (𝒫 ran F \cap Fin) \to w \subseteq ran F$
25	24	adantl	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w \in (𝒫 ran F \cap Fin)) \to w \subseteq ran F$
26		inss2	$⊢ 𝒫 ran F \cap Fin \subseteq Fin$
27	26	sseli	$⊢ w \in (𝒫 ran F \cap Fin) \to w \in Fin$
28	27	adantl	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w \in (𝒫 ran F \cap Fin)) \to w \in Fin$
29		fipreima	$⊢ (F Fn I \land w \subseteq ran F \land w \in Fin) \to \exists v \in (𝒫 I \cap Fin) F [v] = w$
30	21 25 28 29	syl3anc	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w \in (𝒫 ran F \cap Fin)) \to \exists v \in (𝒫 I \cap Fin) F [v] = w$
31		eqcom	$⊢ F [v] = w \leftrightarrow w = F [v]$
32	31	rexbii	$⊢ \exists v \in (𝒫 I \cap Fin) F [v] = w \leftrightarrow \exists v \in (𝒫 I \cap Fin) w = F [v]$
33	30 32	sylib	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w \in (𝒫 ran F \cap Fin)) \to \exists v \in (𝒫 I \cap Fin) w = F [v]$
34		inteq	$⊢ w = F [v] \to ⋂ w = ⋂ F [v]$
35	34	ineq2d	$⊢ w = F [v] \to B \cap ⋂ w = B \cap ⋂ F [v]$
36	35	eqeq2d	$⊢ w = F [v] \to (A = B \cap ⋂ w \leftrightarrow A = B \cap ⋂ F [v])$
37	36	adantl	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land w = F [v]) \to (A = B \cap ⋂ w \leftrightarrow A = B \cap ⋂ F [v])$
38	19 33 37	rexxfrd	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (\exists w \in (𝒫 ran F \cap Fin) A = B \cap ⋂ w \leftrightarrow \exists v \in (𝒫 I \cap Fin) A = B \cap ⋂ F [v])$
39	20	ad2antlr	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to F Fn I$
40		inss1	$⊢ 𝒫 I \cap Fin \subseteq 𝒫 I$
41	40	sseli	$⊢ v \in (𝒫 I \cap Fin) \to v \in 𝒫 I$
42	41	elpwid	$⊢ v \in (𝒫 I \cap Fin) \to v \subseteq I$
43	42	adantl	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to v \subseteq I$
44		imaiinfv	$⊢ (F Fn I \land v \subseteq I) \to ⋂_{y \in v} F (y) = ⋂ F [v]$
45	39 43 44	syl2anc	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to ⋂_{y \in v} F (y) = ⋂ F [v]$
46	45	eqcomd	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to ⋂ F [v] = ⋂_{y \in v} F (y)$
47	46	ineq2d	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to B \cap ⋂ F [v] = B \cap ⋂_{y \in v} F (y)$
48	47	eqeq2d	$⊢ ((B \in V \land F : I ⟶ 𝒫 B) \land v \in (𝒫 I \cap Fin)) \to (A = B \cap ⋂ F [v] \leftrightarrow A = B \cap ⋂_{y \in v} F (y))$
49	48	rexbidva	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (\exists v \in (𝒫 I \cap Fin) A = B \cap ⋂ F [v] \leftrightarrow \exists v \in (𝒫 I \cap Fin) A = B \cap ⋂_{y \in v} F (y))$
50	3 38 49	3bitrd	$⊢ (B \in V \land F : I ⟶ 𝒫 B) \to (A \in fi (\{B\} \cup ran F) \leftrightarrow \exists v \in (𝒫 I \cap Fin) A = B \cap ⋂_{y \in v} F (y))$

Metamath Proof Explorer

Theorem elrfirn

Proof