elfm3

Description: An alternate formulation of elementhood in a mapping filter that requires F to be onto. (Contributed by Jeff Hankins, 1-Oct-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	elfm2.l	$⊢ L = Y filGen B$
	Assertion	elfm3	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (A \in (X FilMap F) (B) \leftrightarrow \exists x \in L A = F [x])$

Proof

Step	Hyp	Ref	Expression
1		elfm2.l	$⊢ L = Y filGen B$
2		foima	$⊢ F : Y \underset{onto}{⟶} X \to F [Y] = X$
3	2	adantl	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to F [Y] = X$
4		fofun	$⊢ F : Y \underset{onto}{⟶} X \to Fun F$
5		elfvdm	$⊢ B \in fBas (Y) \to Y \in dom fBas$
6		funimaexg	$⊢ (Fun F \land Y \in dom fBas) \to F [Y] \in V$
7	4 5 6	syl2anr	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to F [Y] \in V$
8	3 7	eqeltrrd	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to X \in V$
9		fof	$⊢ F : Y \underset{onto}{⟶} X \to F : Y ⟶ X$
10	1	elfm2	$⊢ (X \in V \land B \in fBas (Y) \land F : Y ⟶ X) \to (A \in (X FilMap F) (B) \leftrightarrow (A \subseteq X \land \exists y \in L F [y] \subseteq A))$
11	9 10	syl3an3	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (A \in (X FilMap F) (B) \leftrightarrow (A \subseteq X \land \exists y \in L F [y] \subseteq A))$
12		fgcl	$⊢ B \in fBas (Y) \to Y filGen B \in Fil (Y)$
13	1 12	eqeltrid	$⊢ B \in fBas (Y) \to L \in Fil (Y)$
14	13	3ad2ant2	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to L \in Fil (Y)$
15	14	ad2antrr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to L \in Fil (Y)$
16		simprl	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to y \in L$
17		cnvimass	$⊢ F^{-1} [A] \subseteq dom F$
18		fofn	$⊢ F : Y \underset{onto}{⟶} X \to F Fn Y$
19	18	fndmd	$⊢ F : Y \underset{onto}{⟶} X \to dom F = Y$
20	17 19	sseqtrid	$⊢ F : Y \underset{onto}{⟶} X \to F^{-1} [A] \subseteq Y$
21	20	3ad2ant3	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to F^{-1} [A] \subseteq Y$
22	21	ad2antrr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to F^{-1} [A] \subseteq Y$
23	4	3ad2ant3	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to Fun F$
24	23	ad2antrr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \in L) \to Fun F$
25	1	eleq2i	$⊢ y \in L \leftrightarrow y \in (Y filGen B)$
26		elfg	$⊢ B \in fBas (Y) \to (y \in (Y filGen B) \leftrightarrow (y \subseteq Y \land \exists z \in B z \subseteq y))$
27	26	3ad2ant2	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (y \in (Y filGen B) \leftrightarrow (y \subseteq Y \land \exists z \in B z \subseteq y))$
28	27	adantr	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \to (y \in (Y filGen B) \leftrightarrow (y \subseteq Y \land \exists z \in B z \subseteq y))$
29	25 28	bitrid	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \to (y \in L \leftrightarrow (y \subseteq Y \land \exists z \in B z \subseteq y))$
30	29	simprbda	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \in L) \to y \subseteq Y$
31		sseq2	$⊢ dom F = Y \to (y \subseteq dom F \leftrightarrow y \subseteq Y)$
32	31	biimpar	$⊢ (dom F = Y \land y \subseteq Y) \to y \subseteq dom F$
33	19 32	sylan	$⊢ (F : Y \underset{onto}{⟶} X \land y \subseteq Y) \to y \subseteq dom F$
34	33	3ad2antl3	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land y \subseteq Y) \to y \subseteq dom F$
35	34	adantlr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \subseteq Y) \to y \subseteq dom F$
36	30 35	syldan	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \in L) \to y \subseteq dom F$
37		funimass3	$⊢ (Fun F \land y \subseteq dom F) \to (F [y] \subseteq A \leftrightarrow y \subseteq F^{-1} [A])$
38	24 36 37	syl2anc	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \in L) \to (F [y] \subseteq A \leftrightarrow y \subseteq F^{-1} [A])$
39	38	biimpd	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land y \in L) \to (F [y] \subseteq A \to y \subseteq F^{-1} [A])$
40	39	impr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to y \subseteq F^{-1} [A]$
41		filss	$⊢ (L \in Fil (Y) \land (y \in L \land F^{-1} [A] \subseteq Y \land y \subseteq F^{-1} [A])) \to F^{-1} [A] \in L$
42	15 16 22 40 41	syl13anc	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to F^{-1} [A] \in L$
43		foimacnv	$⊢ (F : Y \underset{onto}{⟶} X \land A \subseteq X) \to F [F^{-1} [A]] = A$
44	43	eqcomd	$⊢ (F : Y \underset{onto}{⟶} X \land A \subseteq X) \to A = F [F^{-1} [A]]$
45	44	3ad2antl3	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \to A = F [F^{-1} [A]]$
46	45	adantr	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to A = F [F^{-1} [A]]$
47		imaeq2	$⊢ x = F^{-1} [A] \to F [x] = F [F^{-1} [A]]$
48	47	rspceeqv	$⊢ (F^{-1} [A] \in L \land A = F [F^{-1} [A]]) \to \exists x \in L A = F [x]$
49	42 46 48	syl2anc	$⊢ (((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \land (y \in L \land F [y] \subseteq A)) \to \exists x \in L A = F [x]$
50	49	rexlimdvaa	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land A \subseteq X) \to (\exists y \in L F [y] \subseteq A \to \exists x \in L A = F [x])$
51	50	expimpd	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to ((A \subseteq X \land \exists y \in L F [y] \subseteq A) \to \exists x \in L A = F [x])$
52		simprr	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to A = F [x]$
53		imassrn	$⊢ F [x] \subseteq ran F$
54		forn	$⊢ F : Y \underset{onto}{⟶} X \to ran F = X$
55	54	3ad2ant3	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to ran F = X$
56	55	adantr	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to ran F = X$
57	53 56	sseqtrid	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to F [x] \subseteq X$
58	52 57	eqsstrd	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to A \subseteq X$
59		eqimss2	$⊢ A = F [x] \to F [x] \subseteq A$
60		imaeq2	$⊢ y = x \to F [y] = F [x]$
61	60	sseq1d	$⊢ y = x \to (F [y] \subseteq A \leftrightarrow F [x] \subseteq A)$
62	61	rspcev	$⊢ (x \in L \land F [x] \subseteq A) \to \exists y \in L F [y] \subseteq A$
63	59 62	sylan2	$⊢ (x \in L \land A = F [x]) \to \exists y \in L F [y] \subseteq A$
64	63	adantl	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to \exists y \in L F [y] \subseteq A$
65	58 64	jca	$⊢ ((X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \land (x \in L \land A = F [x])) \to (A \subseteq X \land \exists y \in L F [y] \subseteq A)$
66	65	rexlimdvaa	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (\exists x \in L A = F [x] \to (A \subseteq X \land \exists y \in L F [y] \subseteq A))$
67	51 66	impbid	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to ((A \subseteq X \land \exists y \in L F [y] \subseteq A) \leftrightarrow \exists x \in L A = F [x])$
68	11 67	bitrd	$⊢ (X \in V \land B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (A \in (X FilMap F) (B) \leftrightarrow \exists x \in L A = F [x])$
69	68	3coml	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X \land X \in V) \to (A \in (X FilMap F) (B) \leftrightarrow \exists x \in L A = F [x])$
70	8 69	mpd3an3	$⊢ (B \in fBas (Y) \land F : Y \underset{onto}{⟶} X) \to (A \in (X FilMap F) (B) \leftrightarrow \exists x \in L A = F [x])$

Metamath Proof Explorer

Theorem elfm3

Proof