ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nqnq0pi GIF version

Theorem nqnq0pi 7436
Description: A nonnegative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
nqnq0pi ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q )

Proof of Theorem nqnq0pi
Dummy variables ๐‘ฃ ๐‘ข ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelxp 4656 . . 3 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โ†” (๐ด โˆˆ N โˆง ๐ต โˆˆ N))
2 vex 2740 . . . . . . 7 ๐‘ฆ โˆˆ V
32elima2 4976 . . . . . 6 (๐‘ฆ โˆˆ ( ~Q0 โ€œ (N ร— N)) โ†” โˆƒ๐‘ฅ(๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฅ ~Q0 ๐‘ฆ))
4 elxp 4643 . . . . . . . . . 10 (๐‘ฅ โˆˆ (N ร— N) โ†” โˆƒ๐‘งโˆƒ๐‘ค(๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)))
54anbi1i 458 . . . . . . . . 9 ((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†” (โˆƒ๐‘งโˆƒ๐‘ค(๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ))
6 19.41vv 1903 . . . . . . . . 9 (โˆƒ๐‘งโˆƒ๐‘ค((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†” (โˆƒ๐‘งโˆƒ๐‘ค(๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ))
75, 6bitr4i 187 . . . . . . . 8 ((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†” โˆƒ๐‘งโˆƒ๐‘ค((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ))
8 simplr 528 . . . . . . . . . . 11 (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N))
9 breq1 4006 . . . . . . . . . . . . 13 (๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โ†’ (๐‘ฅ ~Q0 ๐‘ฆ โ†” โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ))
109adantr 276 . . . . . . . . . . . 12 ((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โ†’ (๐‘ฅ ~Q0 ๐‘ฆ โ†” โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ))
1110biimpa 296 . . . . . . . . . . 11 (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ)
12 id 19 . . . . . . . . . . . 12 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ))
13 enq0er 7433 . . . . . . . . . . . . . . 15 ~Q0 Er (ฯ‰ ร— N)
1413a1i 9 . . . . . . . . . . . . . 14 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ ~Q0 Er (ฯ‰ ร— N))
15 simpr 110 . . . . . . . . . . . . . 14 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ)
1614, 15ercl2 6547 . . . . . . . . . . . . 13 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ (ฯ‰ ร— N))
17 elxp 4643 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ (ฯ‰ ร— N) โ†” โˆƒ๐‘ขโˆƒ๐‘ฃ(๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)))
1816, 17sylib 122 . . . . . . . . . . . 12 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ โˆƒ๐‘ขโˆƒ๐‘ฃ(๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)))
19 19.42vv 1911 . . . . . . . . . . . 12 (โˆƒ๐‘ขโˆƒ๐‘ฃ(((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†” (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง โˆƒ๐‘ขโˆƒ๐‘ฃ(๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))))
2012, 18, 19sylanbrc 417 . . . . . . . . . . 11 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โ†’ โˆƒ๐‘ขโˆƒ๐‘ฃ(((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))))
218, 11, 20syl2anc 411 . . . . . . . . . 10 (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ โˆƒ๐‘ขโˆƒ๐‘ฃ(((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))))
22 simprrl 539 . . . . . . . . . . . . 13 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ข โˆˆ ฯ‰)
23 elni 7306 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ง โˆˆ N โ†” (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ง โ‰  โˆ…))
2423simprbi 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ง โˆˆ N โ†’ ๐‘ง โ‰  โˆ…)
2524neneqd 2368 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ง โˆˆ N โ†’ ยฌ ๐‘ง = โˆ…)
2625ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ยฌ ๐‘ง = โˆ…)
27 elni 7306 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฃ โˆˆ N โ†” (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ฃ โ‰  โˆ…))
2827simprbi 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฃ โˆˆ N โ†’ ๐‘ฃ โ‰  โˆ…)
2928neneqd 2368 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฃ โˆˆ N โ†’ ยฌ ๐‘ฃ = โˆ…)
3029ad2antll 491 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ยฌ ๐‘ฃ = โˆ…)
3126, 30jca 306 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ (ยฌ ๐‘ง = โˆ… โˆง ยฌ ๐‘ฃ = โˆ…))
32 pm4.56 780 . . . . . . . . . . . . . . . . . . . . 21 ((ยฌ ๐‘ง = โˆ… โˆง ยฌ ๐‘ฃ = โˆ…) โ†” ยฌ (๐‘ง = โˆ… โˆจ ๐‘ฃ = โˆ…))
3331, 32sylib 122 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ยฌ (๐‘ง = โˆ… โˆจ ๐‘ฃ = โˆ…))
34 pinn 7307 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ ฯ‰)
3534ad2antrr 488 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ๐‘ง โˆˆ ฯ‰)
36 pinn 7307 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฃ โˆˆ N โ†’ ๐‘ฃ โˆˆ ฯ‰)
3736ad2antll 491 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ๐‘ฃ โˆˆ ฯ‰)
38 nnm00 6530 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ ฯ‰) โ†’ ((๐‘ง ยทo ๐‘ฃ) = โˆ… โ†” (๐‘ง = โˆ… โˆจ ๐‘ฃ = โˆ…)))
3935, 37, 38syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ((๐‘ง ยทo ๐‘ฃ) = โˆ… โ†” (๐‘ง = โˆ… โˆจ ๐‘ฃ = โˆ…)))
4033, 39mtbird 673 . . . . . . . . . . . . . . . . . . 19 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ยฌ (๐‘ง ยทo ๐‘ฃ) = โˆ…)
4140ad2ant2rl 511 . . . . . . . . . . . . . . . . . 18 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ยฌ (๐‘ง ยทo ๐‘ฃ) = โˆ…)
42 breq2 4007 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โ†’ (โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ โ†” โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ))
4342biimpac 298 . . . . . . . . . . . . . . . . . . . . 21 ((โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ โˆง ๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ)
4443ad2ant2lr 510 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ)
45 enq0breq 7434 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ (โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ โ†” (๐‘ง ยทo ๐‘ฃ) = (๐‘ค ยทo ๐‘ข)))
4634, 45sylanl1 402 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ (โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ โ†” (๐‘ง ยทo ๐‘ฃ) = (๐‘ค ยทo ๐‘ข)))
4746ad2ant2rl 511 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ (โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 โŸจ๐‘ข, ๐‘ฃโŸฉ โ†” (๐‘ง ยทo ๐‘ฃ) = (๐‘ค ยทo ๐‘ข)))
4844, 47mpbid 147 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ (๐‘ง ยทo ๐‘ฃ) = (๐‘ค ยทo ๐‘ข))
4948eqeq1d 2186 . . . . . . . . . . . . . . . . . 18 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ((๐‘ง ยทo ๐‘ฃ) = โˆ… โ†” (๐‘ค ยทo ๐‘ข) = โˆ…))
5041, 49mtbid 672 . . . . . . . . . . . . . . . . 17 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ยฌ (๐‘ค ยทo ๐‘ข) = โˆ…)
51 pinn 7307 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค โˆˆ N โ†’ ๐‘ค โˆˆ ฯ‰)
52 nnm00 6530 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ ฯ‰) โ†’ ((๐‘ค ยทo ๐‘ข) = โˆ… โ†” (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…)))
5351, 52sylan 283 . . . . . . . . . . . . . . . . . . 19 ((๐‘ค โˆˆ N โˆง ๐‘ข โˆˆ ฯ‰) โ†’ ((๐‘ค ยทo ๐‘ข) = โˆ… โ†” (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…)))
5453ad2ant2lr 510 . . . . . . . . . . . . . . . . . 18 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N)) โ†’ ((๐‘ค ยทo ๐‘ข) = โˆ… โ†” (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…)))
5554ad2ant2rl 511 . . . . . . . . . . . . . . . . 17 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ((๐‘ค ยทo ๐‘ข) = โˆ… โ†” (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…)))
5650, 55mtbid 672 . . . . . . . . . . . . . . . 16 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ยฌ (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…))
57 pm4.56 780 . . . . . . . . . . . . . . . 16 ((ยฌ ๐‘ค = โˆ… โˆง ยฌ ๐‘ข = โˆ…) โ†” ยฌ (๐‘ค = โˆ… โˆจ ๐‘ข = โˆ…))
5856, 57sylibr 134 . . . . . . . . . . . . . . 15 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ (ยฌ ๐‘ค = โˆ… โˆง ยฌ ๐‘ข = โˆ…))
5958simprd 114 . . . . . . . . . . . . . 14 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ยฌ ๐‘ข = โˆ…)
6059neneqad 2426 . . . . . . . . . . . . 13 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ข โ‰  โˆ…)
61 elni 7306 . . . . . . . . . . . . 13 (๐‘ข โˆˆ N โ†” (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ข โ‰  โˆ…))
6222, 60, 61sylanbrc 417 . . . . . . . . . . . 12 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ข โˆˆ N)
63 simprrr 540 . . . . . . . . . . . 12 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ฃ โˆˆ N)
64 eleq1 2240 . . . . . . . . . . . . . 14 (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โ†’ (๐‘ฆ โˆˆ (N ร— N) โ†” โŸจ๐‘ข, ๐‘ฃโŸฉ โˆˆ (N ร— N)))
65 opelxp 4656 . . . . . . . . . . . . . 14 (โŸจ๐‘ข, ๐‘ฃโŸฉ โˆˆ (N ร— N) โ†” (๐‘ข โˆˆ N โˆง ๐‘ฃ โˆˆ N))
6664, 65bitrdi 196 . . . . . . . . . . . . 13 (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โ†’ (๐‘ฆ โˆˆ (N ร— N) โ†” (๐‘ข โˆˆ N โˆง ๐‘ฃ โˆˆ N)))
6766ad2antrl 490 . . . . . . . . . . . 12 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ (๐‘ฆ โˆˆ (N ร— N) โ†” (๐‘ข โˆˆ N โˆง ๐‘ฃ โˆˆ N)))
6862, 63, 67mpbir2and 944 . . . . . . . . . . 11 ((((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ฆ โˆˆ (N ร— N))
6968exlimivv 1896 . . . . . . . . . 10 (โˆƒ๐‘ขโˆƒ๐‘ฃ(((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง โŸจ๐‘ง, ๐‘คโŸฉ ~Q0 ๐‘ฆ) โˆง (๐‘ฆ = โŸจ๐‘ข, ๐‘ฃโŸฉ โˆง (๐‘ข โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ N))) โ†’ ๐‘ฆ โˆˆ (N ร— N))
7021, 69syl 14 . . . . . . . . 9 (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ (N ร— N))
7170exlimivv 1896 . . . . . . . 8 (โˆƒ๐‘งโˆƒ๐‘ค((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง (๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N)) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ (N ร— N))
727, 71sylbi 121 . . . . . . 7 ((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ (N ร— N))
7372exlimiv 1598 . . . . . 6 (โˆƒ๐‘ฅ(๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฅ ~Q0 ๐‘ฆ) โ†’ ๐‘ฆ โˆˆ (N ร— N))
743, 73sylbi 121 . . . . 5 (๐‘ฆ โˆˆ ( ~Q0 โ€œ (N ร— N)) โ†’ ๐‘ฆ โˆˆ (N ร— N))
7574ssriv 3159 . . . 4 ( ~Q0 โ€œ (N ร— N)) โŠ† (N ร— N)
76 ecinxp 6609 . . . 4 ((( ~Q0 โ€œ (N ร— N)) โŠ† (N ร— N) โˆง โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N)) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ]( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N))))
7775, 76mpan 424 . . 3 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ]( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N))))
781, 77sylbir 135 . 2 ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ]( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N))))
79 enq0enq 7429 . . 3 ~Q = ( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N)))
80 eceq2 6571 . . 3 ( ~Q = ( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N))) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q = [โŸจ๐ด, ๐ตโŸฉ]( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N))))
8179, 80ax-mp 5 . 2 [โŸจ๐ด, ๐ตโŸฉ] ~Q = [โŸจ๐ด, ๐ตโŸฉ]( ~Q0 โˆฉ ((N ร— N) ร— (N ร— N)))
8278, 81eqtr4di 2228 1 ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ [โŸจ๐ด, ๐ตโŸฉ] ~Q0 = [โŸจ๐ด, ๐ตโŸฉ] ~Q )
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148   โ‰  wne 2347   โˆฉ cin 3128   โŠ† wss 3129  โˆ…c0 3422  โŸจcop 3595   class class class wbr 4003  ฯ‰com 4589   ร— cxp 4624   โ€œ cima 4629  (class class class)co 5874   ยทo comu 6414   Er wer 6531  [cec 6532  Ncnpi 7270   ~Q ceq 7277   ~Q0 ceq0 7284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-oadd 6420  df-omul 6421  df-er 6534  df-ec 6536  df-ni 7302  df-mi 7304  df-enq 7345  df-enq0 7422
This theorem is referenced by:  nqnq0  7439  nqpnq0nq  7451  nqnq0a  7452  nqnq0m  7453  prarloclemlo  7492  prarloclemcalc  7500
  Copyright terms: Public domain W3C validator