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 e. { (/) } <-> x = (/) )
4		brtpos0	|- ( y e. _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 e. { (/) } -> ( x tpos F y <-> x F y ) )
11	10	pm5.32i	|- ( ( x e. { (/) } /\ x tpos F y ) <-> ( x e. { (/) } /\ x F y ) )
12		vex	|- y e. _V
13	12	brresi	|- ( x ( tpos F |` { (/) } ) y <-> ( x e. { (/) } /\ x tpos F y ) )
14	12	brresi	|- ( x ( F |` { (/) } ) y <-> ( x e. { (/) } /\ x F y ) )
15	11 13 14	3bitr4i	|- ( x ( tpos F |` { (/) } ) y <-> x ( F |` { (/) } ) y )
16	1 2 15	eqbrriv	|- ( tpos F |` { (/) } ) = ( F |` { (/) } )