Theorem txswaphmeolem

Description: Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	txswaphmeolem	⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
2	1	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑧 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
3		mptresid	⊢ ( I ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑧 )
4		opelxpi	⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
5	4	ancoms	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
6	5	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
7		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) )
8		sneq	⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → { 𝑧 } = { ⟨ 𝑦 , 𝑥 ⟩ } )
9	8	cnveqd	⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ◡ { 𝑧 } = ◡ { ⟨ 𝑦 , 𝑥 ⟩ } )
10	9	unieqd	⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ∪ ◡ { 𝑧 } = ∪ ◡ { ⟨ 𝑦 , 𝑥 ⟩ } )
11		opswap	⊢ ∪ ◡ { ⟨ 𝑦 , 𝑥 ⟩ } = ⟨ 𝑥 , 𝑦 ⟩
12	10 11	eqtrdi	⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ∪ ◡ { 𝑧 } = ⟨ 𝑥 , 𝑦 ⟩ )
13	12	mpompt	⊢ ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
14	13	eqcomi	⊢ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } )
15	14	a1i	⊢ ( ⊤ → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } ) )
16	6 7 15 12	fmpoco	⊢ ( ⊤ → ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) )
17	16	mptru	⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
18	2 3 17	3eqtr4ri	⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) )