fsnex

Description: Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020)

		Ref	Expression
	Hypothesis	fsnex.1	$⊢ x = f (A) \to (ψ \leftrightarrow φ)$
	Assertion	fsnex	$⊢ A \in V \to (\exists f (f : \{A\} ⟶ D \land φ) \leftrightarrow \exists x \in D ψ)$

Proof

Step	Hyp	Ref	Expression
1		fsnex.1	$⊢ x = f (A) \to (ψ \leftrightarrow φ)$
2		fsn2g	$⊢ A \in V \to (f : \{A\} ⟶ D \leftrightarrow (f (A) \in D \land f = \{⟨A, f (A)⟩\}))$
3	2	simprbda	$⊢ (A \in V \land f : \{A\} ⟶ D) \to f (A) \in D$
4	3	adantrr	$⊢ (A \in V \land (f : \{A\} ⟶ D \land φ)) \to f (A) \in D$
5	1	adantl	$⊢ ((A \in V \land (f : \{A\} ⟶ D \land φ)) \land x = f (A)) \to (ψ \leftrightarrow φ)$
6		simprr	$⊢ (A \in V \land (f : \{A\} ⟶ D \land φ)) \to φ$
7	4 5 6	rspcedvd	$⊢ (A \in V \land (f : \{A\} ⟶ D \land φ)) \to \exists x \in D ψ$
8	7	ex	$⊢ A \in V \to ((f : \{A\} ⟶ D \land φ) \to \exists x \in D ψ)$
9	8	exlimdv	$⊢ A \in V \to (\exists f (f : \{A\} ⟶ D \land φ) \to \exists x \in D ψ)$
10	9	imp	$⊢ (A \in V \land \exists f (f : \{A\} ⟶ D \land φ)) \to \exists x \in D ψ$
11		nfv	$⊢ Ⅎ x A \in V$
12		nfre1	$⊢ Ⅎ x \exists x \in D ψ$
13	11 12	nfan	$⊢ Ⅎ x (A \in V \land \exists x \in D ψ)$
14		f1osng	$⊢ (A \in V \land x \in V) \to \{⟨A, x⟩\} : \{A\} \underset{1-1 onto}{⟶} \{x\}$
15	14	elvd	$⊢ A \in V \to \{⟨A, x⟩\} : \{A\} \underset{1-1 onto}{⟶} \{x\}$
16	15	ad3antrrr	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \{⟨A, x⟩\} : \{A\} \underset{1-1 onto}{⟶} \{x\}$
17		f1of	$⊢ \{⟨A, x⟩\} : \{A\} \underset{1-1 onto}{⟶} \{x\} \to \{⟨A, x⟩\} : \{A\} ⟶ \{x\}$
18	16 17	syl	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \{⟨A, x⟩\} : \{A\} ⟶ \{x\}$
19		simplr	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to x \in D$
20	19	snssd	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \{x\} \subseteq D$
21	18 20	fssd	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \{⟨A, x⟩\} : \{A\} ⟶ D$
22		fvsng	$⊢ (A \in V \land x \in V) \to \{⟨A, x⟩\} (A) = x$
23	22	elvd	$⊢ A \in V \to \{⟨A, x⟩\} (A) = x$
24	23	eqcomd	$⊢ A \in V \to x = \{⟨A, x⟩\} (A)$
25	24	ad3antrrr	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to x = \{⟨A, x⟩\} (A)$
26		snex	$⊢ \{⟨A, x⟩\} \in V$
27		feq1	$⊢ f = \{⟨A, x⟩\} \to (f : \{A\} ⟶ D \leftrightarrow \{⟨A, x⟩\} : \{A\} ⟶ D)$
28		fveq1	$⊢ f = \{⟨A, x⟩\} \to f (A) = \{⟨A, x⟩\} (A)$
29	28	eqeq2d	$⊢ f = \{⟨A, x⟩\} \to (x = f (A) \leftrightarrow x = \{⟨A, x⟩\} (A))$
30	27 29	anbi12d	$⊢ f = \{⟨A, x⟩\} \to ((f : \{A\} ⟶ D \land x = f (A)) \leftrightarrow (\{⟨A, x⟩\} : \{A\} ⟶ D \land x = \{⟨A, x⟩\} (A)))$
31	26 30	spcev	$⊢ (\{⟨A, x⟩\} : \{A\} ⟶ D \land x = \{⟨A, x⟩\} (A)) \to \exists f (f : \{A\} ⟶ D \land x = f (A))$
32	21 25 31	syl2anc	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \exists f (f : \{A\} ⟶ D \land x = f (A))$
33		simprl	$⊢ ((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \to f : \{A\} ⟶ D$
34		simpllr	$⊢ (((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \land f : \{A\} ⟶ D) \to ψ$
35		simplrr	$⊢ (((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \land f : \{A\} ⟶ D) \to x = f (A)$
36	35 1	syl	$⊢ (((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \land f : \{A\} ⟶ D) \to (ψ \leftrightarrow φ)$
37	34 36	mpbid	$⊢ (((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \land f : \{A\} ⟶ D) \to φ$
38	33 37	mpdan	$⊢ ((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \to φ$
39	33 38	jca	$⊢ ((((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \land (f : \{A\} ⟶ D \land x = f (A))) \to (f : \{A\} ⟶ D \land φ)$
40	39	ex	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to ((f : \{A\} ⟶ D \land x = f (A)) \to (f : \{A\} ⟶ D \land φ))$
41	40	eximdv	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to (\exists f (f : \{A\} ⟶ D \land x = f (A)) \to \exists f (f : \{A\} ⟶ D \land φ))$
42	32 41	mpd	$⊢ (((A \in V \land \exists x \in D ψ) \land x \in D) \land ψ) \to \exists f (f : \{A\} ⟶ D \land φ)$
43		simpr	$⊢ (A \in V \land \exists x \in D ψ) \to \exists x \in D ψ$
44	13 42 43	r19.29af	$⊢ (A \in V \land \exists x \in D ψ) \to \exists f (f : \{A\} ⟶ D \land φ)$
45	10 44	impbida	$⊢ A \in V \to (\exists f (f : \{A\} ⟶ D \land φ) \leftrightarrow \exists x \in D ψ)$

Metamath Proof Explorer

Theorem fsnex

Proof