Theorem tposres3

Description: The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Hypothesis	tposres2.1	⊢ ( 𝜑 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
Assertion	tposres3	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = tpos ( 𝐹 ↾ ◡ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		tposres2.1	⊢ ( 𝜑 → ¬ ∅ ∈ ( dom 𝐹 ∩ 𝑅 ) )
2	1	tposres2	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) )
3		relcnv	⊢ Rel ◡ dom ( 𝐹 ↾ ◡ 𝑅 )
4		cnvf1o	⊢ ( Rel ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) → ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –1-1-onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) )
5	3 4	ax-mp	⊢ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –1-1-onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 )
6		f1ofo	⊢ ( ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –1-1-onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) → ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) )
7	5 6	ax-mp	⊢ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 )
8		forn	⊢ ( ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) : ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) –onto→ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) → ran ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) = ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) )
9	7 8	ax-mp	⊢ ran ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) = ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 )
10		cnvcnvss	⊢ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ⊆ dom ( 𝐹 ↾ ◡ 𝑅 )
11		resdmss	⊢ dom ( 𝐹 ↾ ◡ 𝑅 ) ⊆ ◡ 𝑅
12	10 11	sstri	⊢ ◡ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ⊆ ◡ 𝑅
13	9 12	eqsstri	⊢ ran ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ◡ 𝑅
14		cores	⊢ ( ran ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ◡ 𝑅 → ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) )
15	13 14	ax-mp	⊢ ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )
16		dftpos6	⊢ tpos ( 𝐹 ↾ ◡ 𝑅 ) = ( ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( { ∅ } × ( ( 𝐹 ↾ ◡ 𝑅 ) “ { ∅ } ) ) )
17		ressn	⊢ ( ( 𝐹 ↾ ◡ 𝑅 ) ↾ { ∅ } ) = ( { ∅ } × ( ( 𝐹 ↾ ◡ 𝑅 ) “ { ∅ } ) )
18		resres	⊢ ( ( 𝐹 ↾ ◡ 𝑅 ) ↾ { ∅ } ) = ( 𝐹 ↾ ( ◡ 𝑅 ∩ { ∅ } ) )
19		relcnv	⊢ Rel ◡ 𝑅
20		0nelrel0	⊢ ( Rel ◡ 𝑅 → ¬ ∅ ∈ ◡ 𝑅 )
21	19 20	ax-mp	⊢ ¬ ∅ ∈ ◡ 𝑅
22		disjsn	⊢ ( ( ◡ 𝑅 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ◡ 𝑅 )
23	21 22	mpbir	⊢ ( ◡ 𝑅 ∩ { ∅ } ) = ∅
24	23	reseq2i	⊢ ( 𝐹 ↾ ( ◡ 𝑅 ∩ { ∅ } ) ) = ( 𝐹 ↾ ∅ )
25		res0	⊢ ( 𝐹 ↾ ∅ ) = ∅
26	18 24 25	3eqtri	⊢ ( ( 𝐹 ↾ ◡ 𝑅 ) ↾ { ∅ } ) = ∅
27	17 26	eqtr3i	⊢ ( { ∅ } × ( ( 𝐹 ↾ ◡ 𝑅 ) “ { ∅ } ) ) = ∅
28	27	uneq2i	⊢ ( ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( { ∅ } × ( ( 𝐹 ↾ ◡ 𝑅 ) “ { ∅ } ) ) ) = ( ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) ∪ ∅ )
29		un0	⊢ ( ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) ) ∪ ∅ ) = ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )
30	16 28 29	3eqtri	⊢ tpos ( 𝐹 ↾ ◡ 𝑅 ) = ( ( 𝐹 ↾ ◡ 𝑅 ) ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )
31		tposrescnv	⊢ ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )
32	15 30 31	3eqtr4ri	⊢ ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) = tpos ( 𝐹 ↾ ◡ 𝑅 )
33	2 32	eqtrdi	⊢ ( 𝜑 → ( tpos 𝐹 ↾ 𝑅 ) = tpos ( 𝐹 ↾ ◡ 𝑅 ) )