f1prex

Description: Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020)

	Ref	Expression
Hypotheses	f1prex.1	$⊢ x = f (A) \to (ψ \leftrightarrow χ)$
	f1prex.2	$⊢ y = f (B) \to (χ \leftrightarrow φ)$
Assertion	f1prex	$⊢ (A \in V \land B \in W \land A \neq B) \to (\exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ) \leftrightarrow \exists x \in D \exists y \in D (x \neq y \land ψ))$

Proof

Step	Hyp	Ref	Expression
1		f1prex.1	$⊢ x = f (A) \to (ψ \leftrightarrow χ)$
2		f1prex.2	$⊢ y = f (B) \to (χ \leftrightarrow φ)$
3		simpl1	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to A \in V$
4		simpl2	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to B \in W$
5		simprl	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to f : \{A, B\} \underset{1-1}{⟶} D$
6		f1f	$⊢ f : \{A, B\} \underset{1-1}{⟶} D \to f : \{A, B\} ⟶ D$
7	5 6	syl	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to f : \{A, B\} ⟶ D$
8		fpr2g	$⊢ (A \in V \land B \in W) \to (f : \{A, B\} ⟶ D \leftrightarrow (f (A) \in D \land f (B) \in D \land f = \{⟨A, f (A)⟩, ⟨B, f (B)⟩\}))$
9	8	biimpa	$⊢ ((A \in V \land B \in W) \land f : \{A, B\} ⟶ D) \to (f (A) \in D \land f (B) \in D \land f = \{⟨A, f (A)⟩, ⟨B, f (B)⟩\})$
10	9	simp1d	$⊢ ((A \in V \land B \in W) \land f : \{A, B\} ⟶ D) \to f (A) \in D$
11	3 4 7 10	syl21anc	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to f (A) \in D$
12	9	simp2d	$⊢ ((A \in V \land B \in W) \land f : \{A, B\} ⟶ D) \to f (B) \in D$
13	3 4 7 12	syl21anc	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to f (B) \in D$
14		prid1g	$⊢ A \in V \to A \in \{A, B\}$
15	3 14	syl	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to A \in \{A, B\}$
16		prid2g	$⊢ B \in W \to B \in \{A, B\}$
17	4 16	syl	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to B \in \{A, B\}$
18	15 17	jca	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to (A \in \{A, B\} \land B \in \{A, B\})$
19		simpl3	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to A \neq B$
20		f1veqaeq	$⊢ (f : \{A, B\} \underset{1-1}{⟶} D \land (A \in \{A, B\} \land B \in \{A, B\})) \to (f (A) = f (B) \to A = B)$
21	20	necon3d	$⊢ (f : \{A, B\} \underset{1-1}{⟶} D \land (A \in \{A, B\} \land B \in \{A, B\})) \to (A \neq B \to f (A) \neq f (B))$
22	21	imp	$⊢ ((f : \{A, B\} \underset{1-1}{⟶} D \land (A \in \{A, B\} \land B \in \{A, B\})) \land A \neq B) \to f (A) \neq f (B)$
23	5 18 19 22	syl21anc	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to f (A) \neq f (B)$
24		simprr	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to φ$
25	23 24	jca	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to (f (A) \neq f (B) \land φ)$
26		neeq1	$⊢ x = f (A) \to (x \neq y \leftrightarrow f (A) \neq y)$
27	26 1	anbi12d	$⊢ x = f (A) \to ((x \neq y \land ψ) \leftrightarrow (f (A) \neq y \land χ))$
28		neeq2	$⊢ y = f (B) \to (f (A) \neq y \leftrightarrow f (A) \neq f (B))$
29	28 2	anbi12d	$⊢ y = f (B) \to ((f (A) \neq y \land χ) \leftrightarrow (f (A) \neq f (B) \land φ))$
30	27 29	rspc2ev	$⊢ (f (A) \in D \land f (B) \in D \land (f (A) \neq f (B) \land φ)) \to \exists x \in D \exists y \in D (x \neq y \land ψ)$
31	11 13 25 30	syl3anc	$⊢ ((A \in V \land B \in W \land A \neq B) \land (f : \{A, B\} \underset{1-1}{⟶} D \land φ)) \to \exists x \in D \exists y \in D (x \neq y \land ψ)$
32	31	ex	$⊢ (A \in V \land B \in W \land A \neq B) \to ((f : \{A, B\} \underset{1-1}{⟶} D \land φ) \to \exists x \in D \exists y \in D (x \neq y \land ψ))$
33	32	exlimdv	$⊢ (A \in V \land B \in W \land A \neq B) \to (\exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ) \to \exists x \in D \exists y \in D (x \neq y \land ψ))$
34		simpll1	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to A \in V$
35		simplrl	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to x \in D$
36	34 35	jca	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to (A \in V \land x \in D)$
37		simpll2	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to B \in W$
38		simplrr	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to y \in D$
39	37 38	jca	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to (B \in W \land y \in D)$
40		simpll3	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to A \neq B$
41		simprl	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to x \neq y$
42		f1oprg	$⊢ ((A \in V \land x \in D) \land (B \in W \land y \in D)) \to ((A \neq B \land x \neq y) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1 onto}{⟶} \{x, y\})$
43	42	imp	$⊢ (((A \in V \land x \in D) \land (B \in W \land y \in D)) \land (A \neq B \land x \neq y)) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1 onto}{⟶} \{x, y\}$
44	36 39 40 41 43	syl22anc	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1 onto}{⟶} \{x, y\}$
45		f1of1	$⊢ \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1 onto}{⟶} \{x, y\} \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} \{x, y\}$
46	44 45	syl	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} \{x, y\}$
47	35 38	prssd	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \{x, y\} \subseteq D$
48		f1ss	$⊢ (\{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} \{x, y\} \land \{x, y\} \subseteq D) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} D$
49	46 47 48	syl2anc	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} D$
50		fvpr1g	$⊢ (A \in V \land x \in D \land A \neq B) \to \{⟨A, x⟩, ⟨B, y⟩\} (A) = x$
51	50	eqcomd	$⊢ (A \in V \land x \in D \land A \neq B) \to x = \{⟨A, x⟩, ⟨B, y⟩\} (A)$
52	34 35 40 51	syl3anc	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to x = \{⟨A, x⟩, ⟨B, y⟩\} (A)$
53		fvpr2g	$⊢ (B \in W \land y \in D \land A \neq B) \to \{⟨A, x⟩, ⟨B, y⟩\} (B) = y$
54	53	eqcomd	$⊢ (B \in W \land y \in D \land A \neq B) \to y = \{⟨A, x⟩, ⟨B, y⟩\} (B)$
55	37 38 40 54	syl3anc	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to y = \{⟨A, x⟩, ⟨B, y⟩\} (B)$
56		prex	$⊢ \{⟨A, x⟩, ⟨B, y⟩\} \in V$
57		f1eq1	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to (f : \{A, B\} \underset{1-1}{⟶} D \leftrightarrow \{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} D)$
58		fveq1	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to f (A) = \{⟨A, x⟩, ⟨B, y⟩\} (A)$
59	58	eqeq2d	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to (x = f (A) \leftrightarrow x = \{⟨A, x⟩, ⟨B, y⟩\} (A))$
60		fveq1	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to f (B) = \{⟨A, x⟩, ⟨B, y⟩\} (B)$
61	60	eqeq2d	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to (y = f (B) \leftrightarrow y = \{⟨A, x⟩, ⟨B, y⟩\} (B))$
62	59 61	anbi12d	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to ((x = f (A) \land y = f (B)) \leftrightarrow (x = \{⟨A, x⟩, ⟨B, y⟩\} (A) \land y = \{⟨A, x⟩, ⟨B, y⟩\} (B)))$
63	57 62	anbi12d	$⊢ f = \{⟨A, x⟩, ⟨B, y⟩\} \to ((f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B))) \leftrightarrow (\{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} D \land (x = \{⟨A, x⟩, ⟨B, y⟩\} (A) \land y = \{⟨A, x⟩, ⟨B, y⟩\} (B))))$
64	56 63	spcev	$⊢ (\{⟨A, x⟩, ⟨B, y⟩\} : \{A, B\} \underset{1-1}{⟶} D \land (x = \{⟨A, x⟩, ⟨B, y⟩\} (A) \land y = \{⟨A, x⟩, ⟨B, y⟩\} (B))) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))$
65	49 52 55 64	syl12anc	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))$
66		simprl	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to f : \{A, B\} \underset{1-1}{⟶} D$
67		simplrr	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to ψ$
68		simprrl	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to x = f (A)$
69	68 1	syl	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to (ψ \leftrightarrow χ)$
70	67 69	mpbid	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to χ$
71		simprrr	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to y = f (B)$
72	71 2	syl	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to (χ \leftrightarrow φ)$
73	70 72	mpbid	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to φ$
74	66 73	jca	$⊢ ((((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \land (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B)))) \to (f : \{A, B\} \underset{1-1}{⟶} D \land φ)$
75	74	ex	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to ((f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B))) \to (f : \{A, B\} \underset{1-1}{⟶} D \land φ))$
76	75	eximdv	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to (\exists f (f : \{A, B\} \underset{1-1}{⟶} D \land (x = f (A) \land y = f (B))) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ))$
77	65 76	mpd	$⊢ (((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \land (x \neq y \land ψ)) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ)$
78	77	ex	$⊢ ((A \in V \land B \in W \land A \neq B) \land (x \in D \land y \in D)) \to ((x \neq y \land ψ) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ))$
79	78	rexlimdvva	$⊢ (A \in V \land B \in W \land A \neq B) \to (\exists x \in D \exists y \in D (x \neq y \land ψ) \to \exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ))$
80	33 79	impbid	$⊢ (A \in V \land B \in W \land A \neq B) \to (\exists f (f : \{A, B\} \underset{1-1}{⟶} D \land φ) \leftrightarrow \exists x \in D \exists y \in D (x \neq y \land ψ))$

Metamath Proof Explorer

Theorem f1prex

Proof