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 𝐹 ↾ { ∅ } ) = ( 𝐹 ↾ { ∅ } )

Proof

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