Theorem f1prex 7282

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

Hypotheses

Ref	Expression
f1prex.1	⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
f1prex.2	⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))

Assertion

Ref	Expression
f1prex	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝐵,𝑓,𝑥,𝑦   𝐷,𝑓,𝑥,𝑦   𝑓,𝑉,𝑥,𝑦   𝑓,𝑊,𝑥,𝑦   𝜒,𝑥   𝜓,𝑓   𝜑,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑓)   𝜓(𝑥,𝑦)   𝜒(𝑦,𝑓)

Proof of Theorem f1prex

Step	Hyp	Ref	Expression
1		simpl1 1208	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
2		simpl2 1209	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ 𝑊)
3		simprl 782	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
4		f1f 6774	. . . . . . 7 ⊢ (𝑓:{𝐴, 𝐵}–1-1→𝐷 → 𝑓:{𝐴, 𝐵}⟶𝐷)
5	3, 4	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}⟶𝐷)
6		fpr2g 7209	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑓:{𝐴, 𝐵}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩})))
7	6	biimpa 481	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩}))
8	7	simp1d 1158	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷)
9	1, 2, 5, 8	syl21anc 850	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷)
10	7	simp2d 1159	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐵) ∈ 𝐷)
11	1, 2, 5, 10	syl21anc 850	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐵) ∈ 𝐷)
12		prid1g 4725	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
13	1, 12	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ {𝐴, 𝐵})
14		prid2g 4726	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵})
15	2, 14	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ {𝐴, 𝐵})
16	13, 15	jca 520	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵}))
17		simpl3 1210	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ≠ 𝐵)
18		f1veqaeq 7254	. . . . . . . . 9 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → ((𝑓‘𝐴) = (𝑓‘𝐵) → 𝐴 = 𝐵))
19	18	necon3d 2977	. . . . . . . 8 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → (𝐴 ≠ 𝐵 → (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
20	19	imp 411	. . . . . . 7 ⊢ (((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) ∧ 𝐴 ≠ 𝐵) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
21	3, 16, 17, 20	syl21anc 850	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
22		simprr 784	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝜑)
23	21, 22	jca 520	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑))
24		neeq1 3018	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ 𝑦))
25		f1prex.1	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
26	24, 25	anbi12d 643	. . . . . 6 ⊢ (𝑥 = (𝑓‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝜓) ↔ ((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒)))
27		neeq2 3019	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → ((𝑓‘𝐴) ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
28		f1prex.2	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))
29	27, 28	anbi12d 643	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝐵) → (((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒) ↔ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)))
30	26, 29	rspc2ev 3593	. . . . 5 ⊢ (((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
31	9, 11, 23, 30	syl3anc 1396	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
32	31	ex 417	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
33	32	exlimdv 1961	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
34		simpll1 1229	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ∈ 𝑉)
35		simplrl 788	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ∈ 𝐷)
36	34, 35	jca 520	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷))
37		simpll2 1230	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐵 ∈ 𝑊)
38		simplrr 789	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 ∈ 𝐷)
39	37, 38	jca 520	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷))
40		simpll3 1231	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ≠ 𝐵)
41		simprl 782	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ≠ 𝑦)
42		f1oprg 6867	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) → ((𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦}))
43	42	imp 411	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
44	36, 39, 40, 41, 43	syl22anc 851	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
45		f1of1 6819	. . . . . . . 8 ⊢ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦} → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
46	44, 45	syl 18	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
47	35, 38	prssd 4787	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {𝑥, 𝑦} ⊆ 𝐷)
48		f1ss 6781	. . . . . . 7 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝐷) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
49	46, 47, 48	syl2anc 595	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
50		fvpr1g 7188	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) = 𝑥)
51	50	eqcomd 2767	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
52	34, 35, 40, 51	syl3anc 1396	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
53		fvpr2g 7189	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
54	53	eqcomd 2767	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
55	37, 38, 40, 54	syl3anc 1396	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
56		prex 5409	. . . . . . 7 ⊢ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ∈ V
57		f1eq1 6769	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷))
58		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
59	58	eqeq2d 2772	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴)))
60		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐵) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
61	60	eqeq2d 2772	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑦 = (𝑓‘𝐵) ↔ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))
62	59, 61	anbi12d 643	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)) ↔ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))))
63	57, 62	anbi12d 643	. . . . . . 7 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) ↔ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))))
64	56, 63	spcev 3564	. . . . . 6 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
65	49, 52, 55, 64	syl12anc 849	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
66		simprl 782	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
67		simplrr 789	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜓)
68		simprrl 792	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑥 = (𝑓‘𝐴))
69	68, 25	syl 18	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜓 ↔ 𝜒))
70	67, 69	mpbid 235	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜒)
71		simprrr 793	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑦 = (𝑓‘𝐵))
72	71, 28	syl 18	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜒 ↔ 𝜑))
73	70, 72	mpbid 235	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜑)
74	66, 73	jca 520	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
75	74	ex 417	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
76	75	eximdv 1945	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
77	65, 76	mpd 16	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
78	77	ex 417	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
79	78	rexlimdvva 3220	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
80	33, 79	impbid 215	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1568  ∃wex 1807   ∈ wcel 2141   ≠ wne 2956  ∃wrex 3087   ⊆ wss 3904  {cpr 4590  ⟨cop 4594  ⟶wf 6532  –1-1→wf1 6533  –1-1-onto→wf1o 6535  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544

This theorem is referenced by:  istrkg3ld  28706