pmtrmvd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pmtrmvd		Structured version Visualization version GIF version

Theorem pmtrmvd 19404

Description: A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)

**Hypothesis**
Ref	Expression
pmtrfval.t	⊢ 𝑇 = (pmTrsp‘𝐷)

**Assertion**
Ref	Expression
pmtrmvd	⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)

Proof of Theorem pmtrmvd Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pmtrfval.t	. . . 4 ⊢ 𝑇 = (pmTrsp‘𝐷)
2	1	pmtrf 19403	. . 3 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → (𝑇‘𝑃):𝐷⟶𝐷)
3		ffn 6716	. . 3 ⊢ ((𝑇‘𝑃):𝐷⟶𝐷 → (𝑇‘𝑃) Fn 𝐷)
4		fndifnfp 7179	. . 3 ⊢ ((𝑇‘𝑃) Fn 𝐷 → dom ((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧})
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → dom ((𝑇‘𝑃) ∖ I ) = {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧})
6	1	pmtrfv 19400	. . . . . 6 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑧) = if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))
7	6	neeq1d 2996	. . . . 5 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧))
8		iffalse 4533	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = 𝑧)
9	8	necon1ai 2964	. . . . . . 7 ⊢ (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 → 𝑧 ∈ 𝑃)
10		iftrue 4530	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧}))
11	10	adantl 481	. . . . . . . . 9 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) = ∪ (𝑃 ∖ {𝑧}))
12		1onn 8654	. . . . . . . . . . 11 ⊢ 1_o ∈ ω
13		simpl3 1191	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈ 2_o)
14		df-2o 8481	. . . . . . . . . . . 12 ⊢ 2_o = suc 1_o
15	13, 14	breqtrdi 5183	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → 𝑃 ≈ suc 1_o)
16		simpr 484	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → 𝑧 ∈ 𝑃)
17		dif1ennn 9179	. . . . . . . . . . 11 ⊢ ((1_o ∈ ω ∧ 𝑃 ≈ suc 1_o ∧ 𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈ 1_o)
18	12, 15, 16, 17	mp3an2i 1463	. . . . . . . . . 10 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → (𝑃 ∖ {𝑧}) ≈ 1_o)
19		en1uniel 9046	. . . . . . . . . 10 ⊢ ((𝑃 ∖ {𝑧}) ≈ 1_o → ∪ (𝑃 ∖ {𝑧}) ∈ (𝑃 ∖ {𝑧}))
20		eldifsni 4789	. . . . . . . . . 10 ⊢ (∪ (𝑃 ∖ {𝑧}) ∈ (𝑃 ∖ {𝑧}) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧)
21	18, 19, 20	3syl 18	. . . . . . . . 9 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → ∪ (𝑃 ∖ {𝑧}) ≠ 𝑧)
22	11, 21	eqnetrd 3004	. . . . . . . 8 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝑃) → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧)
23	22	ex 412	. . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → (𝑧 ∈ 𝑃 → if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧))
24	9, 23	impbid2 225	. . . . . 6 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃))
25	24	adantr 480	. . . . 5 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝐷) → (if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃))
26	7, 25	bitrd 279	. . . 4 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) ∧ 𝑧 ∈ 𝐷) → (((𝑇‘𝑃)‘𝑧) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃))
27	26	rabbidva 3435	. . 3 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃})
28		incom 4197	. . . 4 ⊢ (𝑃 ∩ 𝐷) = (𝐷 ∩ 𝑃)
29		dfin5 3953	. . . 4 ⊢ (𝐷 ∩ 𝑃) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃}
30	28, 29	eqtri 2756	. . 3 ⊢ (𝑃 ∩ 𝐷) = {𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃}
31	27, 30	eqtr4di 2786	. 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → {𝑧 ∈ 𝐷 ∣ ((𝑇‘𝑃)‘𝑧) ≠ 𝑧} = (𝑃 ∩ 𝐷))
32		simp2 1135	. . 3 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → 𝑃 ⊆ 𝐷)
33		df-ss 3962	. . 3 ⊢ (𝑃 ⊆ 𝐷 ↔ (𝑃 ∩ 𝐷) = 𝑃)
34	32, 33	sylib 217	. 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → (𝑃 ∩ 𝐷) = 𝑃)
35	5, 31, 34	3eqtrd 2772	1 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2_o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2936 {crab 3428 ∖ cdif 3942 ∩ cin 3944 ⊆ wss 3945 ifcif 4524 {csn 4624 ∪ cuni 4903 class class class wbr 5142 I cid 5569 dom cdm 5672 suc csuc 6365 Fn wfn 6537 ⟶wf 6538 ‘cfv 6542 ωcom 7864 1_oc1o 8473 2_oc2o 8474 ≈ cen 8954 pmTrspcpmtr 19389

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-om 7865 df-1o 8480 df-2o 8481 df-en 8958 df-pmtr 19390

This theorem is referenced by: pmtrfrn 19406 pmtrfb 19413 symggen 19418 pmtrdifellem2 19425 mdetralt 22503 mdetunilem7 22513 pmtrcnel 32806 pmtrcnel2 32807

W3C validator

	
		OSZAR »