fvimacnvALT

Description: Alternate proof of fvimacnv , based on funimass3 . If funimass3 is ever proved directly, as opposed to using funimacnv pointwise, then the proof of funimacnv should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	fvimacnvALT	$⊢ (Fun F \land A \in dom F) \to (F (A) \in B \leftrightarrow A \in F^{-1} [B])$

Proof

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in dom F \to \{A\} \subseteq dom F$
2		funimass3	$⊢ (Fun F \land \{A\} \subseteq dom F) \to (F [\{A\}] \subseteq B \leftrightarrow \{A\} \subseteq F^{-1} [B])$
3	1 2	sylan2	$⊢ (Fun F \land A \in dom F) \to (F [\{A\}] \subseteq B \leftrightarrow \{A\} \subseteq F^{-1} [B])$
4		fvex	$⊢ F (A) \in V$
5	4	snss	$⊢ F (A) \in B \leftrightarrow \{F (A)\} \subseteq B$
6		eqid	$⊢ dom F = dom F$
7		df-fn	$⊢ F Fn dom F \leftrightarrow (Fun F \land dom F = dom F)$
8	7	biimpri	$⊢ (Fun F \land dom F = dom F) \to F Fn dom F$
9	6 8	mpan2	$⊢ Fun F \to F Fn dom F$
10		fnsnfv	$⊢ (F Fn dom F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
11	9 10	sylan	$⊢ (Fun F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
12	11	sseq1d	$⊢ (Fun F \land A \in dom F) \to (\{F (A)\} \subseteq B \leftrightarrow F [\{A\}] \subseteq B)$
13	5 12	bitrid	$⊢ (Fun F \land A \in dom F) \to (F (A) \in B \leftrightarrow F [\{A\}] \subseteq B)$
14		snssg	$⊢ A \in dom F \to (A \in F^{-1} [B] \leftrightarrow \{A\} \subseteq F^{-1} [B])$
15	14	adantl	$⊢ (Fun F \land A \in dom F) \to (A \in F^{-1} [B] \leftrightarrow \{A\} \subseteq F^{-1} [B])$
16	3 13 15	3bitr4d	$⊢ (Fun F \land A \in dom F) \to (F (A) \in B \leftrightarrow A \in F^{-1} [B])$

Metamath Proof Explorer

Theorem fvimacnvALT

Proof