Theorem f1prex 7136

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 1189	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
2		simpl2 1190	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ 𝑊)
3		simprl 767	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
4		f1f 6654	. . . . . . 7 ⊢ (𝑓:{𝐴, 𝐵}–1-1→𝐷 → 𝑓:{𝐴, 𝐵}⟶𝐷)
5	3, 4	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}⟶𝐷)
6		fpr2g 7069	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑓:{𝐴, 𝐵}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩})))
7	6	biimpa 476	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩}))
8	7	simp1d 1140	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷)
9	1, 2, 5, 8	syl21anc 834	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷)
10	7	simp2d 1141	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐵) ∈ 𝐷)
11	1, 2, 5, 10	syl21anc 834	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐵) ∈ 𝐷)
12		prid1g 4693	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
13	1, 12	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ {𝐴, 𝐵})
14		prid2g 4694	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵})
15	2, 14	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ {𝐴, 𝐵})
16	13, 15	jca 511	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵}))
17		simpl3 1191	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ≠ 𝐵)
18		f1veqaeq 7111	. . . . . . . . 9 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → ((𝑓‘𝐴) = (𝑓‘𝐵) → 𝐴 = 𝐵))
19	18	necon3d 2963	. . . . . . . 8 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → (𝐴 ≠ 𝐵 → (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
20	19	imp 406	. . . . . . 7 ⊢ (((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) ∧ 𝐴 ≠ 𝐵) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
21	3, 16, 17, 20	syl21anc 834	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
22		simprr 769	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝜑)
23	21, 22	jca 511	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑))
24		neeq1 3005	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ 𝑦))
25		f1prex.1	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
26	24, 25	anbi12d 630	. . . . . 6 ⊢ (𝑥 = (𝑓‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝜓) ↔ ((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒)))
27		neeq2 3006	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → ((𝑓‘𝐴) ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
28		f1prex.2	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))
29	27, 28	anbi12d 630	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝐵) → (((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒) ↔ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)))
30	26, 29	rspc2ev 3564	. . . . 5 ⊢ (((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
31	9, 11, 23, 30	syl3anc 1369	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
32	31	ex 412	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
33	32	exlimdv 1937	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
34		simpll1 1210	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ∈ 𝑉)
35		simplrl 773	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ∈ 𝐷)
36	34, 35	jca 511	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷))
37		simpll2 1211	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐵 ∈ 𝑊)
38		simplrr 774	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 ∈ 𝐷)
39	37, 38	jca 511	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷))
40		simpll3 1212	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ≠ 𝐵)
41		simprl 767	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ≠ 𝑦)
42		f1oprg 6744	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) → ((𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦}))
43	42	imp 406	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
44	36, 39, 40, 41, 43	syl22anc 835	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
45		f1of1 6699	. . . . . . . 8 ⊢ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦} → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
46	44, 45	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
47	35, 38	prssd 4752	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {𝑥, 𝑦} ⊆ 𝐷)
48		f1ss 6660	. . . . . . 7 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝐷) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
49	46, 47, 48	syl2anc 583	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
50		fvpr1g 7044	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) = 𝑥)
51	50	eqcomd 2744	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
52	34, 35, 40, 51	syl3anc 1369	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
53		fvpr2g 7045	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
54	53	eqcomd 2744	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
55	37, 38, 40, 54	syl3anc 1369	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
56		prex 5350	. . . . . . 7 ⊢ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ∈ V
57		f1eq1 6649	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷))
58		fveq1 6755	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
59	58	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴)))
60		fveq1 6755	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐵) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
61	60	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑦 = (𝑓‘𝐵) ↔ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))
62	59, 61	anbi12d 630	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)) ↔ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))))
63	57, 62	anbi12d 630	. . . . . . 7 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) ↔ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))))
64	56, 63	spcev 3535	. . . . . 6 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
65	49, 52, 55, 64	syl12anc 833	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
66		simprl 767	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
67		simplrr 774	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜓)
68		simprrl 777	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑥 = (𝑓‘𝐴))
69	68, 25	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜓 ↔ 𝜒))
70	67, 69	mpbid 231	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜒)
71		simprrr 778	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑦 = (𝑓‘𝐵))
72	71, 28	syl 17	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜒 ↔ 𝜑))
73	70, 72	mpbid 231	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜑)
74	66, 73	jca 511	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
75	74	ex 412	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
76	75	eximdv 1921	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
77	65, 76	mpd 15	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
78	77	ex 412	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
79	78	rexlimdvva 3222	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
80	33, 79	impbid 211	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064   ⊆ wss 3883  {cpr 4560  ⟨cop 4564  ⟶wf 6414  –1-1→wf1 6415  –1-1-onto→wf1o 6417  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  istrkg3ld  26726