Theorem f1prex 7156

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 1190	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
2		simpl2 1191	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ 𝑊)
3		simprl 768	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
4		f1f 6670	. . . . . . 7 ⊢ (𝑓:{𝐴, 𝐵}–1-1→𝐷 → 𝑓:{𝐴, 𝐵}⟶𝐷)
5	3, 4	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}⟶𝐷)
6		fpr2g 7087	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑓:{𝐴, 𝐵}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩})))
7	6	biimpa 477	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩}))
8	7	simp1d 1141	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷)
9	1, 2, 5, 8	syl21anc 835	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷)
10	7	simp2d 1142	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐵) ∈ 𝐷)
11	1, 2, 5, 10	syl21anc 835	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐵) ∈ 𝐷)
12		prid1g 4696	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
13	1, 12	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ {𝐴, 𝐵})
14		prid2g 4697	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵})
15	2, 14	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ {𝐴, 𝐵})
16	13, 15	jca 512	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵}))
17		simpl3 1192	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ≠ 𝐵)
18		f1veqaeq 7130	. . . . . . . . 9 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → ((𝑓‘𝐴) = (𝑓‘𝐵) → 𝐴 = 𝐵))
19	18	necon3d 2964	. . . . . . . 8 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → (𝐴 ≠ 𝐵 → (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
20	19	imp 407	. . . . . . 7 ⊢ (((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) ∧ 𝐴 ≠ 𝐵) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
21	3, 16, 17, 20	syl21anc 835	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
22		simprr 770	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝜑)
23	21, 22	jca 512	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑))
24		neeq1 3006	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ 𝑦))
25		f1prex.1	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
26	24, 25	anbi12d 631	. . . . . 6 ⊢ (𝑥 = (𝑓‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝜓) ↔ ((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒)))
27		neeq2 3007	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → ((𝑓‘𝐴) ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
28		f1prex.2	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))
29	27, 28	anbi12d 631	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝐵) → (((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒) ↔ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)))
30	26, 29	rspc2ev 3572	. . . . 5 ⊢ (((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
31	9, 11, 23, 30	syl3anc 1370	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
32	31	ex 413	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
33	32	exlimdv 1936	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
34		simpll1 1211	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ∈ 𝑉)
35		simplrl 774	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ∈ 𝐷)
36	34, 35	jca 512	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷))
37		simpll2 1212	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐵 ∈ 𝑊)
38		simplrr 775	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 ∈ 𝐷)
39	37, 38	jca 512	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷))
40		simpll3 1213	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ≠ 𝐵)
41		simprl 768	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ≠ 𝑦)
42		f1oprg 6761	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) → ((𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦}))
43	42	imp 407	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
44	36, 39, 40, 41, 43	syl22anc 836	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
45		f1of1 6715	. . . . . . . 8 ⊢ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦} → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
46	44, 45	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
47	35, 38	prssd 4755	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {𝑥, 𝑦} ⊆ 𝐷)
48		f1ss 6676	. . . . . . 7 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝐷) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
49	46, 47, 48	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
50		fvpr1g 7062	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) = 𝑥)
51	50	eqcomd 2744	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
52	34, 35, 40, 51	syl3anc 1370	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
53		fvpr2g 7063	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
54	53	eqcomd 2744	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
55	37, 38, 40, 54	syl3anc 1370	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
56		prex 5355	. . . . . . 7 ⊢ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ∈ V
57		f1eq1 6665	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷))
58		fveq1 6773	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
59	58	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴)))
60		fveq1 6773	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐵) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
61	60	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑦 = (𝑓‘𝐵) ↔ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))
62	59, 61	anbi12d 631	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)) ↔ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))))
63	57, 62	anbi12d 631	. . . . . . 7 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) ↔ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))))
64	56, 63	spcev 3545	. . . . . 6 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
65	49, 52, 55, 64	syl12anc 834	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
66		simprl 768	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
67		simplrr 775	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜓)
68		simprrl 778	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑥 = (𝑓‘𝐴))
69	68, 25	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜓 ↔ 𝜒))
70	67, 69	mpbid 231	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜒)
71		simprrr 779	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑦 = (𝑓‘𝐵))
72	71, 28	syl 17	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜒 ↔ 𝜑))
73	70, 72	mpbid 231	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜑)
74	66, 73	jca 512	. . . . . . 7 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
75	74	ex 413	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
76	75	eximdv 1920	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
77	65, 76	mpd 15	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑))
78	77	ex 413	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
79	78	rexlimdvva 3223	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
80	33, 79	impbid 211	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3065   ⊆ wss 3887  {cpr 4563  ⟨cop 4567  ⟶wf 6429  –1-1→wf1 6430  –1-1-onto→wf1o 6432  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441

This theorem is referenced by:  istrkg3ld  26822