| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdcl.s | ⊢ 𝑆  =  ( 𝐼  mPwSer  𝑅 ) | 
						
							| 2 |  | psdcl.b | ⊢ 𝐵  =  ( Base ‘ 𝑆 ) | 
						
							| 3 |  | psdcl.r | ⊢ ( 𝜑  →  𝑅  ∈  Mgm ) | 
						
							| 4 |  | psdcl.x | ⊢ ( 𝜑  →  𝑋  ∈  𝐼 ) | 
						
							| 5 |  | psdcl.f | ⊢ ( 𝜑  →  𝐹  ∈  𝐵 ) | 
						
							| 6 |  | fvexd | ⊢ ( 𝜑  →  ( Base ‘ 𝑅 )  ∈  V ) | 
						
							| 7 |  | ovex | ⊢ ( ℕ0  ↑m  𝐼 )  ∈  V | 
						
							| 8 | 7 | rabex | ⊢ { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∈  V | 
						
							| 9 | 8 | a1i | ⊢ ( 𝜑  →  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∈  V ) | 
						
							| 10 | 3 | adantr | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑅  ∈  Mgm ) | 
						
							| 11 |  | eqid | ⊢ { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  =  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 12 | 11 | psrbagf | ⊢ ( 𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  →  𝑘 : 𝐼 ⟶ ℕ0 ) | 
						
							| 13 | 12 | adantl | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑘 : 𝐼 ⟶ ℕ0 ) | 
						
							| 14 | 4 | adantr | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑋  ∈  𝐼 ) | 
						
							| 15 | 13 14 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑘 ‘ 𝑋 )  ∈  ℕ0 ) | 
						
							| 16 |  | nn0p1nn | ⊢ ( ( 𝑘 ‘ 𝑋 )  ∈  ℕ0  →  ( ( 𝑘 ‘ 𝑋 )  +  1 )  ∈  ℕ ) | 
						
							| 17 | 15 16 | syl | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝑘 ‘ 𝑋 )  +  1 )  ∈  ℕ ) | 
						
							| 18 |  | eqid | ⊢ ( Base ‘ 𝑅 )  =  ( Base ‘ 𝑅 ) | 
						
							| 19 | 1 18 11 2 5 | psrelbas | ⊢ ( 𝜑  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 20 | 19 | adantr | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 21 |  | simpr | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 22 |  | reldmpsr | ⊢ Rel  dom   mPwSer | 
						
							| 23 | 1 2 22 | strov2rcl | ⊢ ( 𝐹  ∈  𝐵  →  𝐼  ∈  V ) | 
						
							| 24 | 5 23 | syl | ⊢ ( 𝜑  →  𝐼  ∈  V ) | 
						
							| 25 |  | 1nn0 | ⊢ 1  ∈  ℕ0 | 
						
							| 26 | 11 | snifpsrbag | ⊢ ( ( 𝐼  ∈  V  ∧  1  ∈  ℕ0 )  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 27 | 24 25 26 | sylancl | ⊢ ( 𝜑  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 28 | 27 | adantr | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 29 | 11 | psrbagaddcl | ⊢ ( ( 𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∧  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 30 | 21 28 29 | syl2anc | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 31 | 20 30 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) | 
						
							| 32 |  | eqid | ⊢ ( .g ‘ 𝑅 )  =  ( .g ‘ 𝑅 ) | 
						
							| 33 | 18 32 | mulgnncl | ⊢ ( ( 𝑅  ∈  Mgm  ∧  ( ( 𝑘 ‘ 𝑋 )  +  1 )  ∈  ℕ  ∧  ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 ) )  →  ( ( ( 𝑘 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) | 
						
							| 34 | 10 17 31 33 | syl3anc | ⊢ ( ( 𝜑  ∧  𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑘 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) | 
						
							| 35 | 34 | fmpttd | ⊢ ( 𝜑  →  ( 𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑘 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 36 | 6 9 35 | elmapdd | ⊢ ( 𝜑  →  ( 𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑘 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  ∈  ( ( Base ‘ 𝑅 )  ↑m  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) ) | 
						
							| 37 | 1 2 11 4 5 | psdval | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  =  ( 𝑘  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑘 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 38 | 1 18 11 2 24 | psrbas | ⊢ ( 𝜑  →  𝐵  =  ( ( Base ‘ 𝑅 )  ↑m  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) ) | 
						
							| 39 | 36 37 38 | 3eltr4d | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∈  𝐵 ) |