isoval

Description: The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 21-May-2020)

	Ref	Expression
Hypotheses	invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	isoval.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion	isoval	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		invss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		isoval.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
7		isofval	⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ ( Inv ‘ 𝐶 ) ) )
8	3 7	syl	⊢ ( 𝜑 → ( Iso ‘ 𝐶 ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ ( Inv ‘ 𝐶 ) ) )
9	2	coeq2i	⊢ ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ ( Inv ‘ 𝐶 ) )
10	8 6 9	3eqtr4g	⊢ ( 𝜑 → 𝐼 = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) )
11	10	oveqd	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = ( 𝑋 ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) 𝑌 ) )
12		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
13		ovex	⊢ ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∈ V
14	13	inex1	⊢ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V
15	12 14	fnmpoi	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( 𝐵 × 𝐵 )
16		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
17	1 2 3 16	invffval	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
18	17	fneq1d	⊢ ( 𝜑 → ( 𝑁 Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( 𝐵 × 𝐵 ) ) )
19	15 18	mpbiri	⊢ ( 𝜑 → 𝑁 Fn ( 𝐵 × 𝐵 ) )
20	4 5	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
21		fvco2	⊢ ( ( 𝑁 Fn ( 𝐵 × 𝐵 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) ) → ( ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
22	19 20 21	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
23		df-ov	⊢ ( 𝑋 ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) 𝑌 ) = ( ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
24		ovex	⊢ ( 𝑋 𝑁 𝑌 ) ∈ V
25		dmeq	⊢ ( 𝑧 = ( 𝑋 𝑁 𝑌 ) → dom 𝑧 = dom ( 𝑋 𝑁 𝑌 ) )
26		eqid	⊢ ( 𝑧 ∈ V ↦ dom 𝑧 ) = ( 𝑧 ∈ V ↦ dom 𝑧 )
27	24	dmex	⊢ dom ( 𝑋 𝑁 𝑌 ) ∈ V
28	25 26 27	fvmpt	⊢ ( ( 𝑋 𝑁 𝑌 ) ∈ V → ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑋 𝑁 𝑌 ) ) = dom ( 𝑋 𝑁 𝑌 ) )
29	24 28	ax-mp	⊢ ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑋 𝑁 𝑌 ) ) = dom ( 𝑋 𝑁 𝑌 )
30		df-ov	⊢ ( 𝑋 𝑁 𝑌 ) = ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
31	30	fveq2i	⊢ ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑋 𝑁 𝑌 ) ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
32	29 31	eqtr3i	⊢ dom ( 𝑋 𝑁 𝑌 ) = ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ‘ ( 𝑁 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
33	22 23 32	3eqtr4g	⊢ ( 𝜑 → ( 𝑋 ( ( 𝑧 ∈ V ↦ dom 𝑧 ) ∘ 𝑁 ) 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )
34	11 33	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )

Metamath Proof Explorer

Theorem isoval

Proof