tposideq

Description: Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025)

		Ref	Expression
	Assertion	tposideq	⊢ ( Rel 𝑅 → ( tpos I ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		tposres	⊢ ( Rel 𝑅 → ( tpos I ↾ 𝑅 ) = tpos ( I ↾ ^◡ 𝑅 ) )
2		relcnv	⊢ Rel ^◡ 𝑅
3		fnresi	⊢ ( I ↾ ^◡ 𝑅 ) Fn ^◡ 𝑅
4		tposfn2	⊢ ( Rel ^◡ 𝑅 → ( ( I ↾ ^◡ 𝑅 ) Fn ^◡ 𝑅 → tpos ( I ↾ ^◡ 𝑅 ) Fn ^◡ ^◡ 𝑅 ) )
5	2 3 4	mp2	⊢ tpos ( I ↾ ^◡ 𝑅 ) Fn ^◡ ^◡ 𝑅
6		dfrel2	⊢ ( Rel 𝑅 ↔ ^◡ ^◡ 𝑅 = 𝑅 )
7	6	biimpi	⊢ ( Rel 𝑅 → ^◡ ^◡ 𝑅 = 𝑅 )
8	7	fneq2d	⊢ ( Rel 𝑅 → ( tpos ( I ↾ ^◡ 𝑅 ) Fn ^◡ ^◡ 𝑅 ↔ tpos ( I ↾ ^◡ 𝑅 ) Fn 𝑅 ) )
9	5 8	mpbii	⊢ ( Rel 𝑅 → tpos ( I ↾ ^◡ 𝑅 ) Fn 𝑅 )
10		vsnex	⊢ { 𝑥 } ∈ V
11	10	cnvex	⊢ ^◡ { 𝑥 } ∈ V
12	11	uniex	⊢ ∪ ^◡ { 𝑥 } ∈ V
13		eqid	⊢ ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } )
14	12 13	fnmpti	⊢ ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) Fn 𝑅
15	14	a1i	⊢ ( Rel 𝑅 → ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) Fn 𝑅 )
16		1st2nd	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
17		1st2ndb	⊢ ( 𝑦 ∈ ( V × V ) ↔ 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
18	17	biimpri	⊢ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → 𝑦 ∈ ( V × V ) )
19		2nd1st	⊢ ( 𝑦 ∈ ( V × V ) → ∪ ^◡ { 𝑦 } = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
20	16 18 19	3syl	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ∪ ^◡ { 𝑦 } = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
21		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
22	21	cnveqd	⊢ ( 𝑥 = 𝑦 → ^◡ { 𝑥 } = ^◡ { 𝑦 } )
23	22	unieqd	⊢ ( 𝑥 = 𝑦 → ∪ ^◡ { 𝑥 } = ∪ ^◡ { 𝑦 } )
24	23 13 12	fvmpt3i	⊢ ( 𝑦 ∈ 𝑅 → ( ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) ‘ 𝑦 ) = ∪ ^◡ { 𝑦 } )
25	24	adantl	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) ‘ 𝑦 ) = ∪ ^◡ { 𝑦 } )
26	16	fveq2d	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( tpos ( I ↾ ^◡ 𝑅 ) ‘ 𝑦 ) = ( tpos ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) )
27		ovtpos	⊢ ( ( 1^st ‘ 𝑦 ) tpos ( I ↾ ^◡ 𝑅 ) ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝑦 ) ( I ↾ ^◡ 𝑅 ) ( 1^st ‘ 𝑦 ) )
28		df-ov	⊢ ( ( 1^st ‘ 𝑦 ) tpos ( I ↾ ^◡ 𝑅 ) ( 2^nd ‘ 𝑦 ) ) = ( tpos ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
29		df-ov	⊢ ( ( 2^nd ‘ 𝑦 ) ( I ↾ ^◡ 𝑅 ) ( 1^st ‘ 𝑦 ) ) = ( ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
30	27 28 29	3eqtr3i	⊢ ( tpos ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) = ( ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
31	30	a1i	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( tpos ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) = ( ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ) )
32		simpr	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → 𝑦 ∈ 𝑅 )
33	16 32	eqeltrrd	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ 𝑅 )
34		fvex	⊢ ( 2^nd ‘ 𝑦 ) ∈ V
35		fvex	⊢ ( 1^st ‘ 𝑦 ) ∈ V
36	34 35	opelcnv	⊢ ( ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ∈ ^◡ 𝑅 ↔ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ 𝑅 )
37	36	biimpri	⊢ ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ 𝑅 → ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ∈ ^◡ 𝑅 )
38		fvresi	⊢ ( ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ∈ ^◡ 𝑅 → ( ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
39	33 37 38	3syl	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( ( I ↾ ^◡ 𝑅 ) ‘ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
40	26 31 39	3eqtrd	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( tpos ( I ↾ ^◡ 𝑅 ) ‘ 𝑦 ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
41	20 25 40	3eqtr4rd	⊢ ( ( Rel 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( tpos ( I ↾ ^◡ 𝑅 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) ‘ 𝑦 ) )
42	9 15 41	eqfnfvd	⊢ ( Rel 𝑅 → tpos ( I ↾ ^◡ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) )
43	1 42	eqtrd	⊢ ( Rel 𝑅 → ( tpos I ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ∪ ^◡ { 𝑥 } ) )

Metamath Proof Explorer

Theorem tposideq

Proof