Theorem f1prex 7018

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 1188	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
2		simpl2 1189	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ 𝑊)
3		simprl 770	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
4		f1f 6549	. . . . . . 7 ⊢ (𝑓:{𝐴, 𝐵}–1-1→𝐷 → 𝑓:{𝐴, 𝐵}⟶𝐷)
5	3, 4	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}⟶𝐷)
6		fpr2g 6951	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑓:{𝐴, 𝐵}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩})))
7	6	biimpa 480	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩}))
8	7	simp1d 1139	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷)
9	1, 2, 5, 8	syl21anc 836	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷)
10	7	simp2d 1140	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐵) ∈ 𝐷)
11	1, 2, 5, 10	syl21anc 836	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐵) ∈ 𝐷)
12		prid1g 4656	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
13	1, 12	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ {𝐴, 𝐵})
14		prid2g 4657	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵})
15	2, 14	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ {𝐴, 𝐵})
16	13, 15	jca 515	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵}))
17		simpl3 1190	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ≠ 𝐵)
18		f1veqaeq 6993	. . . . . . . . 9 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → ((𝑓‘𝐴) = (𝑓‘𝐵) → 𝐴 = 𝐵))
19	18	necon3d 3008	. . . . . . . 8 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → (𝐴 ≠ 𝐵 → (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
20	19	imp 410	. . . . . . 7 ⊢ (((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) ∧ 𝐴 ≠ 𝐵) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
21	3, 16, 17, 20	syl21anc 836	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
22		simprr 772	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝜑)
23	21, 22	jca 515	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑))
24		neeq1 3049	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ 𝑦))
25		f1prex.1	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
26	24, 25	anbi12d 633	. . . . . 6 ⊢ (𝑥 = (𝑓‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝜓) ↔ ((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒)))
27		neeq2 3050	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → ((𝑓‘𝐴) ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
28		f1prex.2	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))
29	27, 28	anbi12d 633	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝐵) → (((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒) ↔ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)))
30	26, 29	rspc2ev 3583	. . . . 5 ⊢ (((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
31	9, 11, 23, 30	syl3anc 1368	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
32	31	ex 416	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
33	32	exlimdv 1934	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
34		simpll1 1209	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ∈ 𝑉)
35		simplrl 776	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ∈ 𝐷)
36	34, 35	jca 515	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷))
37		simpll2 1210	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐵 ∈ 𝑊)
38		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 ∈ 𝐷)
39	37, 38	jca 515	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷))
40		simpll3 1211	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ≠ 𝐵)
41		simprl 770	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ≠ 𝑦)
42		f1oprg 6634	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) → ((𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦}))
43	42	imp 410	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
44	36, 39, 40, 41, 43	syl22anc 837	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
45		f1of1 6589	. . . . . . . 8 ⊢ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦} → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
46	44, 45	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
47	35, 38	prssd 4715	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {𝑥, 𝑦} ⊆ 𝐷)
48		f1ss 6555	. . . . . . 7 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝐷) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
49	46, 47, 48	syl2anc 587	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
50		fvpr1g 6931	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) = 𝑥)
51	50	eqcomd 2804	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
52	34, 35, 40, 51	syl3anc 1368	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
53		fvpr2g 6932	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
54	53	eqcomd 2804	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
55	37, 38, 40, 54	syl3anc 1368	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
56		prex 5298	. . . . . . 7 ⊢ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ∈ V
57		f1eq1 6544	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷))
58		fveq1 6644	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
59	58	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴)))
60		fveq1 6644	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐵) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
61	60	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑦 = (𝑓‘𝐵) ↔ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))
62	59, 61	anbi12d 633	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)) ↔ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))))
63	57, 62	anbi12d 633	. . . . . . 7 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) ↔ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))))
64	56, 63	spcev 3555	. . . . . 6 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
65	49, 52, 55, 64	syl12anc 835	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
66		simprl 770	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
67		simplrr 777	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜓)
68		simprrl 780	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑥 = (𝑓‘𝐴))
69	68, 25	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜓 ↔ 𝜒))
70	67, 69	mpbid 235	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜒)
71		simprrr 781	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑦 = (𝑓‘𝐵))
72	71, 28	syl 17	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜒 ↔ 𝜑))
73	70, 72	mpbid 235	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜑)
74	66, 73	jca 515	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
75	74	ex 416	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
76	75	eximdv 1918	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
77	65, 76	mpd 15	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
78	77	ex 416	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
79	78	rexlimdvva 3253	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
80	33, 79	impbid 215	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107   ⊆ wss 3881  {cpr 4527  ⟨cop 4531  ⟶wf 6320  –1-1→wf1 6321  –1-1-onto→wf1o 6323  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332

This theorem is referenced by:  istrkg3ld  26255