This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ { 𝐴 } ) = ∅