Theorem pmtrrn2 19256

Description: For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)

Hypotheses

Ref	Expression
pmtrrn.t	⊢ 𝑇 = (pmTrsp‘𝐷)
pmtrrn.r	⊢ 𝑅 = ran 𝑇

Assertion

Ref	Expression
pmtrrn2	⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))

Distinct variable groups:   𝑥,𝑦,𝐷   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦

Proof of Theorem pmtrrn2

Step	Hyp	Ref	Expression
1		pmtrrn.t	. . . . . . 7 ⊢ 𝑇 = (pmTrsp‘𝐷)
2		pmtrrn.r	. . . . . . 7 ⊢ 𝑅 = ran 𝑇
3		eqid 2731	. . . . . . 7 ⊢ dom (𝐹 ∖ I ) = dom (𝐹 ∖ I )
4	1, 2, 3	pmtrfrn 19254	. . . . . 6 ⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o) ∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I ))))
5	4	simpld 495	. . . . 5 ⊢ (𝐹 ∈ 𝑅 → (𝐷 ∈ V ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o))
6	5	simp3d 1144	. . . 4 ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≈ 2o)
7		en2 9232	. . . 4 ⊢ (dom (𝐹 ∖ I ) ≈ 2o → ∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦})
8	6, 7	syl 17	. . 3 ⊢ (𝐹 ∈ 𝑅 → ∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦})
9	5	simp2d 1143	. . . . . . 7 ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ⊆ 𝐷)
10	4	simprd 496	. . . . . . 7 ⊢ (𝐹 ∈ 𝑅 → 𝐹 = (𝑇‘dom (𝐹 ∖ I )))
11	9, 6, 10	jca32 516	. . . . . 6 ⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ (dom (𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I )))))
12		sseq1 3972	. . . . . . 7 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → (dom (𝐹 ∖ I ) ⊆ 𝐷 ↔ {𝑥, 𝑦} ⊆ 𝐷))
13		breq1 5113	. . . . . . . 8 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → (dom (𝐹 ∖ I ) ≈ 2o ↔ {𝑥, 𝑦} ≈ 2o))
14		fveq2 6847	. . . . . . . . 9 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → (𝑇‘dom (𝐹 ∖ I )) = (𝑇‘{𝑥, 𝑦}))
15	14	eqeq2d 2742	. . . . . . . 8 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → (𝐹 = (𝑇‘dom (𝐹 ∖ I )) ↔ 𝐹 = (𝑇‘{𝑥, 𝑦})))
16	13, 15	anbi12d 631	. . . . . . 7 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ((dom (𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I ))) ↔ ({𝑥, 𝑦} ≈ 2o ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))
17	12, 16	anbi12d 631	. . . . . 6 ⊢ (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ((dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ (dom (𝐹 ∖ I ) ≈ 2o ∧ 𝐹 = (𝑇‘dom (𝐹 ∖ I )))) ↔ ({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2o ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))))
18	11, 17	syl5ibcom 244	. . . . 5 ⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2o ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))))
19		vex 3450	. . . . . . . 8 ⊢ 𝑥 ∈ V
20		vex 3450	. . . . . . . 8 ⊢ 𝑦 ∈ V
21	19, 20	prss 4785	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ {𝑥, 𝑦} ⊆ 𝐷)
22	21	bicomi 223	. . . . . 6 ⊢ ({𝑥, 𝑦} ⊆ 𝐷 ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷))
23		pr2ne 9949	. . . . . . . 8 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ({𝑥, 𝑦} ≈ 2o ↔ 𝑥 ≠ 𝑦))
24	23	el2v 3454	. . . . . . 7 ⊢ ({𝑥, 𝑦} ≈ 2o ↔ 𝑥 ≠ 𝑦)
25	24	anbi1i 624	. . . . . 6 ⊢ (({𝑥, 𝑦} ≈ 2o ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})) ↔ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))
26	22, 25	anbi12i 627	. . . . 5 ⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ({𝑥, 𝑦} ≈ 2o ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))
27	18, 26	syl6ib 250	. . . 4 ⊢ (𝐹 ∈ 𝑅 → (dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))))
28	27	2eximdv 1922	. . 3 ⊢ (𝐹 ∈ 𝑅 → (∃𝑥∃𝑦dom (𝐹 ∖ I ) = {𝑥, 𝑦} → ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))))
29	8, 28	mpd 15	. 2 ⊢ (𝐹 ∈ 𝑅 → ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))
30		r2ex 3188	. 2 ⊢ (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))))
31	29, 30	sylibr 233	1 ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2939  ∃wrex 3069  Vcvv 3446   ∖ cdif 3910   ⊆ wss 3913  {cpr 4593   class class class wbr 5110   I cid 5535  dom cdm 5638  ran crn 5639  ‘cfv 6501  2_oc2o 8411   ≈ cen 8887  pmTrspcpmtr 19237

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-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  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-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  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-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-1o 8417  df-2o 8418  df-en 8891  df-pmtr 19238

This theorem is referenced by:  mdetunilem7  22004