Theorem f1prex 7235

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 1191	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
2		simpl2 1192	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ 𝑊)
3		simprl 769	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
4		f1f 6743	. . . . . . 7 ⊢ (𝑓:{𝐴, 𝐵}–1-1→𝐷 → 𝑓:{𝐴, 𝐵}⟶𝐷)
5	3, 4	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝑓:{𝐴, 𝐵}⟶𝐷)
6		fpr2g 7166	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑓:{𝐴, 𝐵}⟶𝐷 ↔ ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩})))
7	6	biimpa 477	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → ((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ 𝑓 = {⟨𝐴, (𝑓‘𝐴)⟩, ⟨𝐵, (𝑓‘𝐵)⟩}))
8	7	simp1d 1142	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐴) ∈ 𝐷)
9	1, 2, 5, 8	syl21anc 836	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ∈ 𝐷)
10	7	simp2d 1143	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓:{𝐴, 𝐵}⟶𝐷) → (𝑓‘𝐵) ∈ 𝐷)
11	1, 2, 5, 10	syl21anc 836	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐵) ∈ 𝐷)
12		prid1g 4726	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
13	1, 12	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ∈ {𝐴, 𝐵})
14		prid2g 4727	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵})
15	2, 14	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐵 ∈ {𝐴, 𝐵})
16	13, 15	jca 512	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵}))
17		simpl3 1193	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝐴 ≠ 𝐵)
18		f1veqaeq 7209	. . . . . . . . 9 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → ((𝑓‘𝐴) = (𝑓‘𝐵) → 𝐴 = 𝐵))
19	18	necon3d 2960	. . . . . . . 8 ⊢ ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) → (𝐴 ≠ 𝐵 → (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
20	19	imp 407	. . . . . . 7 ⊢ (((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝐴 ∈ {𝐴, 𝐵} ∧ 𝐵 ∈ {𝐴, 𝐵})) ∧ 𝐴 ≠ 𝐵) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
21	3, 16, 17, 20	syl21anc 836	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → (𝑓‘𝐴) ≠ (𝑓‘𝐵))
22		simprr 771	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → 𝜑)
23	21, 22	jca 512	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑))
24		neeq1 3002	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ 𝑦))
25		f1prex.1	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒))
26	24, 25	anbi12d 631	. . . . . 6 ⊢ (𝑥 = (𝑓‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝜓) ↔ ((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒)))
27		neeq2 3003	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → ((𝑓‘𝐴) ≠ 𝑦 ↔ (𝑓‘𝐴) ≠ (𝑓‘𝐵)))
28		f1prex.2	. . . . . . 7 ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑))
29	27, 28	anbi12d 631	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝐵) → (((𝑓‘𝐴) ≠ 𝑦 ∧ 𝜒) ↔ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)))
30	26, 29	rspc2ev 3593	. . . . 5 ⊢ (((𝑓‘𝐴) ∈ 𝐷 ∧ (𝑓‘𝐵) ∈ 𝐷 ∧ ((𝑓‘𝐴) ≠ (𝑓‘𝐵) ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
31	9, 11, 23, 30	syl3anc 1371	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))
32	31	ex 413	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
33	32	exlimdv 1936	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))
34		simpll1 1212	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ∈ 𝑉)
35		simplrl 775	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ∈ 𝐷)
36	34, 35	jca 512	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷))
37		simpll2 1213	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐵 ∈ 𝑊)
38		simplrr 776	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 ∈ 𝐷)
39	37, 38	jca 512	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷))
40		simpll3 1214	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝐴 ≠ 𝐵)
41		simprl 769	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 ≠ 𝑦)
42		f1oprg 6834	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) → ((𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦}))
43	42	imp 407	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) ∧ (𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐴 ≠ 𝐵 ∧ 𝑥 ≠ 𝑦)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
44	36, 39, 40, 41, 43	syl22anc 837	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦})
45		f1of1 6788	. . . . . . . 8 ⊢ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1-onto→{𝑥, 𝑦} → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
46	44, 45	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦})
47	35, 38	prssd 4787	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {𝑥, 𝑦} ⊆ 𝐷)
48		f1ss 6749	. . . . . . 7 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝐷) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
49	46, 47, 48	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷)
50		fvpr1g 7141	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) = 𝑥)
51	50	eqcomd 2737	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
52	34, 35, 40, 51	syl3anc 1371	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
53		fvpr2g 7142	. . . . . . . 8 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
54	53	eqcomd 2737	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
55	37, 38, 40, 54	syl3anc 1371	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
56		prex 5394	. . . . . . 7 ⊢ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ∈ V
57		f1eq1 6738	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓:{𝐴, 𝐵}–1-1→𝐷 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷))
58		fveq1 6846	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐴) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴))
59	58	eqeq2d 2742	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑥 = (𝑓‘𝐴) ↔ 𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴)))
60		fveq1 6846	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑓‘𝐵) = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))
61	60	eqeq2d 2742	. . . . . . . . 9 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝑦 = (𝑓‘𝐵) ↔ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))
62	59, 61	anbi12d 631	. . . . . . . 8 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)) ↔ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))))
63	57, 62	anbi12d 631	. . . . . . 7 ⊢ (𝑓 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → ((𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))) ↔ ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵)))))
64	56, 63	spcev 3566	. . . . . 6 ⊢ (({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐴) ∧ 𝑦 = ({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}‘𝐵))) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
65	49, 52, 55, 64	syl12anc 835	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵))))
66		simprl 769	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑓:{𝐴, 𝐵}–1-1→𝐷)
67		simplrr 776	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜓)
68		simprrl 779	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝑥 = (𝑓‘𝐴))
69	68, 25	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → (𝜓 ↔ 𝜒))
70	67, 69	mpbid 231	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝑥 ≠ 𝑦 ∧ 𝜓)) ∧ (𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ (𝑥 = (𝑓‘𝐴) ∧ 𝑦 = (𝑓‘𝐵)))) → 𝜒)
71		simprrr 780	. . . . . . . . . 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 3201	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓) → ∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑)))
80	33, 79	impbid 211	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2939  ∃wrex 3069   ⊆ wss 3913  {cpr 4593  ⟨cop 4597  ⟶wf 6497  –1-1→wf1 6498  –1-1-onto→wf1o 6500  ‘cfv 6501

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509

This theorem is referenced by:  istrkg3ld  27466