Metamath Proof Explorer


Theorem onmsuc

Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onmsuc ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo suc ๐ต ) = ( ( ๐ด ยทo ๐ต ) +o ๐ด ) )

Proof

Step Hyp Ref Expression
1 peano2 โŠข ( ๐ต โˆˆ ฯ‰ โ†’ suc ๐ต โˆˆ ฯ‰ )
2 nnon โŠข ( suc ๐ต โˆˆ ฯ‰ โ†’ suc ๐ต โˆˆ On )
3 1 2 syl โŠข ( ๐ต โˆˆ ฯ‰ โ†’ suc ๐ต โˆˆ On )
4 omv โŠข ( ( ๐ด โˆˆ On โˆง suc ๐ต โˆˆ On ) โ†’ ( ๐ด ยทo suc ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ suc ๐ต ) )
5 3 4 sylan2 โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo suc ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ suc ๐ต ) )
6 1 adantl โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ suc ๐ต โˆˆ ฯ‰ )
7 6 fvresd โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ suc ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ suc ๐ต ) )
8 5 7 eqtr4d โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo suc ๐ต ) = ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ suc ๐ต ) )
9 ovex โŠข ( ๐ด ยทo ๐ต ) โˆˆ V
10 oveq1 โŠข ( ๐‘ฅ = ( ๐ด ยทo ๐ต ) โ†’ ( ๐‘ฅ +o ๐ด ) = ( ( ๐ด ยทo ๐ต ) +o ๐ด ) )
11 eqid โŠข ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) = ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) )
12 ovex โŠข ( ( ๐ด ยทo ๐ต ) +o ๐ด ) โˆˆ V
13 10 11 12 fvmpt โŠข ( ( ๐ด ยทo ๐ต ) โˆˆ V โ†’ ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ๐ด ยทo ๐ต ) ) = ( ( ๐ด ยทo ๐ต ) +o ๐ด ) )
14 9 13 ax-mp โŠข ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ๐ด ยทo ๐ต ) ) = ( ( ๐ด ยทo ๐ต ) +o ๐ด )
15 nnon โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ๐ต โˆˆ On )
16 omv โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ On ) โ†’ ( ๐ด ยทo ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ ๐ต ) )
17 15 16 sylan2 โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ ๐ต ) )
18 fvres โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ ๐ต ) )
19 18 adantl โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) = ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ€˜ ๐ต ) )
20 17 19 eqtr4d โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo ๐ต ) = ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) )
21 20 fveq2d โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ๐ด ยทo ๐ต ) ) = ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) ) )
22 14 21 eqtr3id โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( ๐ด ยทo ๐ต ) +o ๐ด ) = ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) ) )
23 frsuc โŠข ( ๐ต โˆˆ ฯ‰ โ†’ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ suc ๐ต ) = ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) ) )
24 23 adantl โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ suc ๐ต ) = ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) โ€˜ ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ ๐ต ) ) )
25 22 24 eqtr4d โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( ๐ด ยทo ๐ต ) +o ๐ด ) = ( ( rec ( ( ๐‘ฅ โˆˆ V โ†ฆ ( ๐‘ฅ +o ๐ด ) ) , โˆ… ) โ†พ ฯ‰ ) โ€˜ suc ๐ต ) )
26 8 25 eqtr4d โŠข ( ( ๐ด โˆˆ On โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo suc ๐ต ) = ( ( ๐ด ยทo ๐ต ) +o ๐ด ) )