Metamath Proof Explorer


Theorem funcringcsetclem4ALTV

Description: Lemma 4 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses funcringcsetcALTV.r 𝑅 = ( RingCatALTV ‘ 𝑈 )
funcringcsetcALTV.s 𝑆 = ( SetCat ‘ 𝑈 )
funcringcsetcALTV.b 𝐵 = ( Base ‘ 𝑅 )
funcringcsetcALTV.c 𝐶 = ( Base ‘ 𝑆 )
funcringcsetcALTV.u ( 𝜑𝑈 ∈ WUni )
funcringcsetcALTV.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcringcsetcALTV.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
Assertion funcringcsetclem4ALTV ( 𝜑𝐺 Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV.r 𝑅 = ( RingCatALTV ‘ 𝑈 )
2 funcringcsetcALTV.s 𝑆 = ( SetCat ‘ 𝑈 )
3 funcringcsetcALTV.b 𝐵 = ( Base ‘ 𝑅 )
4 funcringcsetcALTV.c 𝐶 = ( Base ‘ 𝑆 )
5 funcringcsetcALTV.u ( 𝜑𝑈 ∈ WUni )
6 funcringcsetcALTV.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcringcsetcALTV.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
8 eqid ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) )
9 ovex ( 𝑥 RingHom 𝑦 ) ∈ V
10 id ( ( 𝑥 RingHom 𝑦 ) ∈ V → ( 𝑥 RingHom 𝑦 ) ∈ V )
11 10 resiexd ( ( 𝑥 RingHom 𝑦 ) ∈ V → ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ∈ V )
12 9 11 ax-mp ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ∈ V
13 8 12 fnmpoi ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) Fn ( 𝐵 × 𝐵 )
14 7 fneq1d ( 𝜑 → ( 𝐺 Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) Fn ( 𝐵 × 𝐵 ) ) )
15 13 14 mpbiri ( 𝜑𝐺 Fn ( 𝐵 × 𝐵 ) )