MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnmordi Structured version   Visualization version   GIF version

Theorem nnmordi 8633
Description: Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
nnmordi (((๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))

Proof of Theorem nnmordi
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elnn 7868 . . . . . 6 ((๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ ฯ‰) โ†’ ๐ด โˆˆ ฯ‰)
21expcom 412 . . . . 5 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ ๐ด โˆˆ ฯ‰))
3 eleq2 2820 . . . . . . . . . . 11 (๐‘ฅ = ๐ต โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐ต))
4 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = ๐ต โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo ๐ต))
54eleq2d 2817 . . . . . . . . . . 11 (๐‘ฅ = ๐ต โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))
63, 5imbi12d 343 . . . . . . . . . 10 (๐‘ฅ = ๐ต โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))
76imbi2d 339 . . . . . . . . 9 (๐‘ฅ = ๐ต โ†’ ((((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ))) โ†” (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
8 eleq2 2820 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ โˆ…))
9 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo โˆ…))
109eleq2d 2817 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…)))
118, 10imbi12d 343 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…))))
12 eleq2 2820 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐‘ฆ))
13 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ฆ โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo ๐‘ฆ))
1413eleq2d 2817 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))
1512, 14imbi12d 343 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ))))
16 eleq2 2820 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ suc ๐‘ฆ))
17 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo suc ๐‘ฆ))
1817eleq2d 2817 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ)))
1916, 18imbi12d 343 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))
20 noel 4329 . . . . . . . . . . . 12 ยฌ ๐ด โˆˆ โˆ…
2120pm2.21i 119 . . . . . . . . . . 11 (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…))
2221a1i 11 . . . . . . . . . 10 (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…)))
23 elsuci 6430 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ))
24 nnmcl 8614 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰)
25 simpl 481 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐ถ โˆˆ ฯ‰)
2624, 25jca 510 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰))
27 nnaword1 8631 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐‘ฆ) โŠ† ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
2827sseld 3980 . . . . . . . . . . . . . . . . . . . . 21 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ) โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
2928imim2d 57 . . . . . . . . . . . . . . . . . . . 20 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))))
3029imp 405 . . . . . . . . . . . . . . . . . . 19 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ))) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3130adantrl 712 . . . . . . . . . . . . . . . . . 18 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
32 nna0 8606 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) = (๐ถ ยทo ๐‘ฆ))
3332ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) = (๐ถ ยทo ๐‘ฆ))
34 nnaordi 8620 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ ฯ‰ โˆง (๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3534ancoms 457 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3635imp 405 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
3733, 36eqeltrrd 2832 . . . . . . . . . . . . . . . . . . . 20 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ ยทo ๐‘ฆ) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
38 oveq2 7419 . . . . . . . . . . . . . . . . . . . . 21 (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐‘ฆ))
3938eleq1d 2816 . . . . . . . . . . . . . . . . . . . 20 (๐ด = ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ) โ†” (๐ถ ยทo ๐‘ฆ) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4037, 39syl5ibrcom 246 . . . . . . . . . . . . . . . . . . 19 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4140adantrr 713 . . . . . . . . . . . . . . . . . 18 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4231, 41jaod 855 . . . . . . . . . . . . . . . . 17 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ ((๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ) โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4326, 42sylan 578 . . . . . . . . . . . . . . . 16 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ ((๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ) โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4423, 43syl5 34 . . . . . . . . . . . . . . 15 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
45 nnmsuc 8609 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ถ ยทo suc ๐‘ฆ) = ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
4645eleq2d 2817 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ) โ†” (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4746adantr 479 . . . . . . . . . . . . . . 15 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ) โ†” (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4844, 47sylibrd 258 . . . . . . . . . . . . . 14 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ)))
4948exp43 435 . . . . . . . . . . . . 13 (๐ถ โˆˆ ฯ‰ โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5049com12 32 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5150adantld 489 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5251impd 409 . . . . . . . . . 10 (๐‘ฆ โˆˆ ฯ‰ โ†’ (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ)))))
5311, 15, 19, 22, 52finds2 7893 . . . . . . . . 9 (๐‘ฅ โˆˆ ฯ‰ โ†’ (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ))))
547, 53vtoclga 3565 . . . . . . . 8 (๐ต โˆˆ ฯ‰ โ†’ (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))
5554com23 86 . . . . . . 7 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))
5655exp4a 430 . . . . . 6 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ ((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
5756exp4a 430 . . . . 5 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ด โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))))
582, 57mpdd 43 . . . 4 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
5958com34 91 . . 3 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
6059com24 95 . 2 (๐ต โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
6160imp31 416 1 (((๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 843   = wceq 1539   โˆˆ wcel 2104  โˆ…c0 4321  suc csuc 6365  (class class class)co 7411  ฯ‰com 7857   +o coa 8465   ยทo comu 8466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-oadd 8472  df-omul 8473
This theorem is referenced by:  nnmord  8634  mulclpi  10890
  Copyright terms: Public domain W3C validator