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 414 . . . . 5 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ ๐ด โˆˆ ฯ‰))
3 eleq2 2822 . . . . . . . . . . 11 (๐‘ฅ = ๐ต โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐ต))
4 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = ๐ต โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo ๐ต))
54eleq2d 2819 . . . . . . . . . . 11 (๐‘ฅ = ๐ต โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))
63, 5imbi12d 344 . . . . . . . . . 10 (๐‘ฅ = ๐ต โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))
76imbi2d 340 . . . . . . . . 9 (๐‘ฅ = ๐ต โ†’ ((((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ))) โ†” (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
8 eleq2 2822 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ โˆ…))
9 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo โˆ…))
109eleq2d 2819 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…)))
118, 10imbi12d 344 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…))))
12 eleq2 2822 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ ๐‘ฆ))
13 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ฆ โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo ๐‘ฆ))
1413eleq2d 2819 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))
1512, 14imbi12d 344 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ))))
16 eleq2 2822 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฅ โ†” ๐ด โˆˆ suc ๐‘ฆ))
17 oveq2 7419 . . . . . . . . . . . 12 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ถ ยทo ๐‘ฅ) = (๐ถ ยทo suc ๐‘ฆ))
1817eleq2d 2819 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ) โ†” (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ)))
1916, 18imbi12d 344 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ด โˆˆ ๐‘ฅ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฅ)) โ†” (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))
20 noel 4330 . . . . . . . . . . . 12 ยฌ ๐ด โˆˆ โˆ…
2120pm2.21i 119 . . . . . . . . . . 11 (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…))
2221a1i 11 . . . . . . . . . 10 (((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ โˆ… โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo โˆ…)))
23 elsuci 6431 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ))
24 nnmcl 8614 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰)
25 simpl 483 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐ถ โˆˆ ฯ‰)
2624, 25jca 512 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰))
27 nnaword1 8631 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (๐ถ ยทo ๐‘ฆ) โŠ† ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
2827sseld 3981 . . . . . . . . . . . . . . . . . . . . 21 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ) โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
2928imim2d 57 . . . . . . . . . . . . . . . . . . . 20 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))))
3029imp 407 . . . . . . . . . . . . . . . . . . 19 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ))) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3130adantrl 714 . . . . . . . . . . . . . . . . . 18 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
32 nna0 8606 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) = (๐ถ ยทo ๐‘ฆ))
3332ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) = (๐ถ ยทo ๐‘ฆ))
34 nnaordi 8620 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ถ โˆˆ ฯ‰ โˆง (๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3534ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
3635imp 407 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ ((๐ถ ยทo ๐‘ฆ) +o โˆ…) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
3733, 36eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . 20 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ถ ยทo ๐‘ฆ) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ))
38 oveq2 7419 . . . . . . . . . . . . . . . . . . . . 21 (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐‘ฆ))
3938eleq1d 2818 . . . . . . . . . . . . . . . . . . . 20 (๐ด = ๐‘ฆ โ†’ ((๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ) โ†” (๐ถ ยทo ๐‘ฆ) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4037, 39syl5ibrcom 246 . . . . . . . . . . . . . . . . . . 19 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4140adantrr 715 . . . . . . . . . . . . . . . . . 18 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด = ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4231, 41jaod 857 . . . . . . . . . . . . . . . . 17 ((((๐ถ ยทo ๐‘ฆ) โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ ((๐ด โˆˆ ๐‘ฆ โˆจ ๐ด = ๐‘ฆ) โ†’ (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4326, 42sylan 580 . . . . . . . . . . . . . . . 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 2819 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ) โ†” (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4746adantr 481 . . . . . . . . . . . . . . 15 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ ((๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ) โ†” (๐ถ ยทo ๐ด) โˆˆ ((๐ถ ยทo ๐‘ฆ) +o ๐ถ)))
4844, 47sylibrd 258 . . . . . . . . . . . . . 14 (((๐ถ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (โˆ… โˆˆ ๐ถ โˆง (๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)))) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ)))
4948exp43 437 . . . . . . . . . . . . 13 (๐ถ โˆˆ ฯ‰ โ†’ (๐‘ฆ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5049com12 32 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5150adantld 491 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ ((๐ด โˆˆ ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐‘ฆ)) โ†’ (๐ด โˆˆ suc ๐‘ฆ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo suc ๐‘ฆ))))))
5251impd 411 . . . . . . . . . 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 432 . . . . . 6 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ ((๐ด โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
5756exp4a 432 . . . . 5 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ด โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต))))))
582, 57mpdd 43 . . . 4 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
5958com34 91 . . 3 (๐ต โˆˆ ฯ‰ โ†’ (๐ด โˆˆ ๐ต โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
6059com24 95 . 2 (๐ต โˆˆ ฯ‰ โ†’ (๐ถ โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ ๐ถ โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))))
6160imp31 418 1 (((๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰) โˆง โˆ… โˆˆ ๐ถ) โ†’ (๐ด โˆˆ ๐ต โ†’ (๐ถ ยทo ๐ด) โˆˆ (๐ถ ยทo ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   = wceq 1541   โˆˆ wcel 2106  โˆ…c0 4322  suc csuc 6366  (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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  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