Theorem pmtrsn 19426

Description: The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for 𝐴 ∉ V, i.e. for the empty set {𝐴} = ∅ resulting in (pmTrsp‘∅) = ∅. (Contributed by AV, 6-Aug-2019.)

Assertion

Ref	Expression
pmtrsn	⊢ (pmTrsp‘{𝐴}) = ∅

Proof of Theorem pmtrsn

Dummy variables 𝑝 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 5369	. . 3 ⊢ {𝐴} ∈ V
2		eqid 2731	. . . 4 ⊢ (pmTrsp‘{𝐴}) = (pmTrsp‘{𝐴})
3	2	pmtrfval 19357	. . 3 ⊢ ({𝐴} ∈ V → (pmTrsp‘{𝐴}) = (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
4	1, 3	ax-mp 5	. 2 ⊢ (pmTrsp‘{𝐴}) = (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))
5		eqid 2731	. . . . 5 ⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))
6	5	dmmpt 6182	. . . 4 ⊢ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = {𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V}
7		2on0 8394	. . . . . . . . 9 ⊢ 2o ≠ ∅
8		ensymb 8919	. . . . . . . . . 10 ⊢ (∅ ≈ 2o ↔ 2o ≈ ∅)
9		en0 8935	. . . . . . . . . 10 ⊢ (2o ≈ ∅ ↔ 2o = ∅)
10	8, 9	bitri 275	. . . . . . . . 9 ⊢ (∅ ≈ 2o ↔ 2o = ∅)
11	7, 10	nemtbir 3024	. . . . . . . 8 ⊢ ¬ ∅ ≈ 2o
12		snnen2o 9124	. . . . . . . 8 ⊢ ¬ {𝐴} ≈ 2o
13		0ex 5240	. . . . . . . . 9 ⊢ ∅ ∈ V
14		breq1 5089	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (𝑦 ≈ 2o ↔ ∅ ≈ 2o))
15	14	notbid 318	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (¬ 𝑦 ≈ 2o ↔ ¬ ∅ ≈ 2o))
16		breq1 5089	. . . . . . . . . 10 ⊢ (𝑦 = {𝐴} → (𝑦 ≈ 2o ↔ {𝐴} ≈ 2o))
17	16	notbid 318	. . . . . . . . 9 ⊢ (𝑦 = {𝐴} → (¬ 𝑦 ≈ 2o ↔ ¬ {𝐴} ≈ 2o))
18	13, 1, 15, 17	ralpr 4648	. . . . . . . 8 ⊢ (∀𝑦 ∈ {∅, {𝐴}} ¬ 𝑦 ≈ 2o ↔ (¬ ∅ ≈ 2o ∧ ¬ {𝐴} ≈ 2o))
19	11, 12, 18	mpbir2an 711	. . . . . . 7 ⊢ ∀𝑦 ∈ {∅, {𝐴}} ¬ 𝑦 ≈ 2o
20		pwsn 4847	. . . . . . . 8 ⊢ 𝒫 {𝐴} = {∅, {𝐴}}
21	20	raleqi 3290	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝒫 {𝐴} ¬ 𝑦 ≈ 2o ↔ ∀𝑦 ∈ {∅, {𝐴}} ¬ 𝑦 ≈ 2o)
22	19, 21	mpbir 231	. . . . . 6 ⊢ ∀𝑦 ∈ 𝒫 {𝐴} ¬ 𝑦 ≈ 2o
23		rabeq0 4333	. . . . . 6 ⊢ ({𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} = ∅ ↔ ∀𝑦 ∈ 𝒫 {𝐴} ¬ 𝑦 ≈ 2o)
24	22, 23	mpbir 231	. . . . 5 ⊢ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} = ∅
25	24	rabeqi 3408	. . . 4 ⊢ {𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} = {𝑝 ∈ ∅ ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V}
26		rab0 4331	. . . 4 ⊢ {𝑝 ∈ ∅ ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} = ∅
27	6, 25, 26	3eqtri 2758	. . 3 ⊢ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅
28		mptrel 5760	. . . 4 ⊢ Rel (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))
29		reldm0 5863	. . . 4 ⊢ (Rel (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → ((𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ ↔ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅))
30	28, 29	ax-mp 5	. . 3 ⊢ ((𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ ↔ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅)
31	27, 30	mpbir 231	. 2 ⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅
32	4, 31	eqtri 2754	1 ⊢ (pmTrsp‘{𝐴}) = ∅

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047  {crab 3395  Vcvv 3436   ∖ cdif 3894  ∅c0 4278  ifcif 4470  𝒫 cpw 4545  {csn 4571  {cpr 4573  ∪ cuni 4854   class class class wbr 5086   ↦ cmpt 5167  dom cdm 5611  Rel wrel 5616  ‘cfv 6476  2_oc2o 8374   ≈ cen 8861  pmTrspcpmtr 19348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-1o 8380  df-2o 8381  df-er 8617  df-en 8865  df-pmtr 19349

This theorem is referenced by:  psgnsn  19427