Theorem pmtrsn

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 A e/ _V , i.e. for the empty set { A } = (/) resulting in ( pmTrsp(/) ) = (/) . (Contributed by AV, 6-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 𝐴 } ∈ V
2		eqid	⊢ ( pmTrsp ‘ { 𝐴 } ) = ( pmTrsp ‘ { 𝐴 } )
3	2	pmtrfval	⊢ ( { 𝐴 } ∈ V → ( pmTrsp ‘ { 𝐴 } ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
4	1 3	ax-mp	⊢ ( pmTrsp ‘ { 𝐴 } ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
5		eqid	⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
6	5	dmmpt	⊢ dom ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = { 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ∣ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V }
7		2on0	⊢ 2o ≠ ∅
8		ensymb	⊢ ( ∅ ≈ 2o ↔ 2o ≈ ∅ )
9		en0	⊢ ( 2o ≈ ∅ ↔ 2o = ∅ )
10	8 9	bitri	⊢ ( ∅ ≈ 2o ↔ 2o = ∅ )
11	7 10	nemtbir	⊢ ¬ ∅ ≈ 2o
12		snnen2o	⊢ ¬ { 𝐴 } ≈ 2o
13		0ex	⊢ ∅ ∈ V
14		breq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ≈ 2o ↔ ∅ ≈ 2o ) )
15	14	notbid	⊢ ( 𝑦 = ∅ → ( ¬ 𝑦 ≈ 2o ↔ ¬ ∅ ≈ 2o ) )
16		breq1	⊢ ( 𝑦 = { 𝐴 } → ( 𝑦 ≈ 2o ↔ { 𝐴 } ≈ 2o ) )
17	16	notbid	⊢ ( 𝑦 = { 𝐴 } → ( ¬ 𝑦 ≈ 2o ↔ ¬ { 𝐴 } ≈ 2o ) )
18	13 1 15 17	ralpr	⊢ ( ∀ 𝑦 ∈ { ∅ , { 𝐴 } } ¬ 𝑦 ≈ 2o ↔ ( ¬ ∅ ≈ 2o ∧ ¬ { 𝐴 } ≈ 2o ) )
19	11 12 18	mpbir2an	⊢ ∀ 𝑦 ∈ { ∅ , { 𝐴 } } ¬ 𝑦 ≈ 2o
20		pwsn	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }
21	20	raleqi	⊢ ( ∀ 𝑦 ∈ 𝒫 { 𝐴 } ¬ 𝑦 ≈ 2o ↔ ∀ 𝑦 ∈ { ∅ , { 𝐴 } } ¬ 𝑦 ≈ 2o )
22	19 21	mpbir	⊢ ∀ 𝑦 ∈ 𝒫 { 𝐴 } ¬ 𝑦 ≈ 2o
23		rabeq0	⊢ ( { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } = ∅ ↔ ∀ 𝑦 ∈ 𝒫 { 𝐴 } ¬ 𝑦 ≈ 2o )
24	22 23	mpbir	⊢ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } = ∅
25	24	rabeqi	⊢ { 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ∣ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V } = { 𝑝 ∈ ∅ ∣ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V }
26		rab0	⊢ { 𝑝 ∈ ∅ ∣ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V } = ∅
27	6 25 26	3eqtri	⊢ dom ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅
28		mptrel	⊢ Rel ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
29		reldm0	⊢ ( Rel ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ( ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅ ↔ dom ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅ ) )
30	28 29	ax-mp	⊢ ( ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅ ↔ dom ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅ )
31	27 30	mpbir	⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 { 𝐴 } ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ { 𝐴 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ∅
32	4 31	eqtri	⊢ ( pmTrsp ‘ { 𝐴 } ) = ∅