fnexALT

Description: Alternate proof of fnex , derived using the Axiom of Replacement in the form of funimaexg . This version uses ax-pow and ax-un , whereas fnex does not. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	fnexALT	$⊢ (F Fn A \land A \in B) \to F \in V$

Proof

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		relssdmrn	$⊢ Rel F \to F \subseteq dom F \times ran F$
3	1 2	syl	$⊢ F Fn A \to F \subseteq dom F \times ran F$
4	3	adantr	$⊢ (F Fn A \land A \in B) \to F \subseteq dom F \times ran F$
5		fndm	$⊢ F Fn A \to dom F = A$
6	5	eleq1d	$⊢ F Fn A \to (dom F \in B \leftrightarrow A \in B)$
7	6	biimpar	$⊢ (F Fn A \land A \in B) \to dom F \in B$
8		fnfun	$⊢ F Fn A \to Fun F$
9		funimaexg	$⊢ (Fun F \land A \in B) \to F [A] \in V$
10	8 9	sylan	$⊢ (F Fn A \land A \in B) \to F [A] \in V$
11		imadmrn	$⊢ F [dom F] = ran F$
12	5	imaeq2d	$⊢ F Fn A \to F [dom F] = F [A]$
13	11 12	eqtr3id	$⊢ F Fn A \to ran F = F [A]$
14	13	eleq1d	$⊢ F Fn A \to (ran F \in V \leftrightarrow F [A] \in V)$
15	14	biimpar	$⊢ (F Fn A \land F [A] \in V) \to ran F \in V$
16	10 15	syldan	$⊢ (F Fn A \land A \in B) \to ran F \in V$
17		xpexg	$⊢ (dom F \in B \land ran F \in V) \to dom F \times ran F \in V$
18	7 16 17	syl2anc	$⊢ (F Fn A \land A \in B) \to dom F \times ran F \in V$
19		ssexg	$⊢ (F \subseteq dom F \times ran F \land dom F \times ran F \in V) \to F \in V$
20	4 18 19	syl2anc	$⊢ (F Fn A \land A \in B) \to F \in V$

Metamath Proof Explorer

Theorem fnexALT

Proof