Metamath Proof Explorer

Theorem tposres0

Description: The transposition of a set restricted to the empty set is the set restricted to the empty set. See also ressn and dftpos6 for an alternate proof. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion tposres0 ⊢ tpos F ↾ ∅ = F ↾ ∅

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ tpos F ↾ ∅
2 relres ⊢ Rel ⁡ F ↾ ∅
3 velsn ⊢ x ∈ ∅ ↔ x = ∅
4 brtpos0 ⊢ y ∈ V → ∅ tpos F y ↔ ∅ F y
5 4 elv ⊢ ∅ tpos F y ↔ ∅ F y
6 breq1 ⊢ x = ∅ → x tpos F y ↔ ∅ tpos F y
7 breq1 ⊢ x = ∅ → x F y ↔ ∅ F y
8 6 7 bibi12d ⊢ x = ∅ → x tpos F y ↔ x F y ↔ ∅ tpos F y ↔ ∅ F y
9 5 8 mpbiri ⊢ x = ∅ → x tpos F y ↔ x F y
10 3 9 sylbi ⊢ x ∈ ∅ → x tpos F y ↔ x F y
11 10 pm5.32i ⊢ x ∈ ∅ ∧ x tpos F y ↔ x ∈ ∅ ∧ x F y
12 vex ⊢ y ∈ V
13 12 brresi ⊢ x tpos F ↾ ∅ y ↔ x ∈ ∅ ∧ x tpos F y
14 12 brresi ⊢ x F ↾ ∅ y ↔ x ∈ ∅ ∧ x F y
15 11 13 14 3bitr4i ⊢ x tpos F ↾ ∅ y ↔ x F ↾ ∅ y
16 1 2 15 eqbrriv ⊢ tpos F ↾ ∅ = F ↾ ∅