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

Theorem nqnq0pi 6593
 Description: A non-negative 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 4401 . . 3 (⟨𝐴, 𝐵⟩ ∈ (N × N) ↔ (𝐴N𝐵N))
2 vex 2577 . . . . . . 7 𝑦 ∈ V
32elima2 4701 . . . . . 6 (𝑦 ∈ ( ~Q0 “ (N × N)) ↔ ∃𝑥(𝑥 ∈ (N × N) ∧ 𝑥 ~Q0 𝑦))
4 elxp 4389 . . . . . . . . . 10 (𝑥 ∈ (N × N) ↔ ∃𝑧𝑤(𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)))
54anbi1i 439 . . . . . . . . 9 ((𝑥 ∈ (N × N) ∧ 𝑥 ~Q0 𝑦) ↔ (∃𝑧𝑤(𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦))
6 19.41vv 1799 . . . . . . . . 9 (∃𝑧𝑤((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) ↔ (∃𝑧𝑤(𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦))
75, 6bitr4i 180 . . . . . . . 8 ((𝑥 ∈ (N × N) ∧ 𝑥 ~Q0 𝑦) ↔ ∃𝑧𝑤((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦))
8 simplr 490 . . . . . . . . . . 11 (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) → (𝑧N𝑤N))
9 breq1 3794 . . . . . . . . . . . . 13 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑥 ~Q0 𝑦 ↔ ⟨𝑧, 𝑤⟩ ~Q0 𝑦))
109adantr 265 . . . . . . . . . . . 12 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) → (𝑥 ~Q0 𝑦 ↔ ⟨𝑧, 𝑤⟩ ~Q0 𝑦))
1110biimpa 284 . . . . . . . . . . 11 (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) → ⟨𝑧, 𝑤⟩ ~Q0 𝑦)
12 id 19 . . . . . . . . . . . 12 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → ((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦))
13 enq0er 6590 . . . . . . . . . . . . . . 15 ~Q0 Er (ω × N)
1413a1i 9 . . . . . . . . . . . . . 14 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → ~Q0 Er (ω × N))
15 simpr 107 . . . . . . . . . . . . . 14 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → ⟨𝑧, 𝑤⟩ ~Q0 𝑦)
1614, 15ercl2 6149 . . . . . . . . . . . . 13 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → 𝑦 ∈ (ω × N))
17 elxp 4389 . . . . . . . . . . . . 13 (𝑦 ∈ (ω × N) ↔ ∃𝑢𝑣(𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N)))
1816, 17sylib 131 . . . . . . . . . . . 12 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → ∃𝑢𝑣(𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N)))
19 19.42vv 1804 . . . . . . . . . . . 12 (∃𝑢𝑣(((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) ↔ (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ ∃𝑢𝑣(𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))))
2012, 18, 19sylanbrc 402 . . . . . . . . . . 11 (((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) → ∃𝑢𝑣(((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))))
218, 11, 20syl2anc 397 . . . . . . . . . 10 (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) → ∃𝑢𝑣(((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))))
22 simprrl 499 . . . . . . . . . . . . 13 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑢 ∈ ω)
23 elni 6463 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧N ↔ (𝑧 ∈ ω ∧ 𝑧 ≠ ∅))
2423simprbi 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧N𝑧 ≠ ∅)
2524neneqd 2241 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧N → ¬ 𝑧 = ∅)
2625ad2antrr 465 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ¬ 𝑧 = ∅)
27 elni 6463 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣N ↔ (𝑣 ∈ ω ∧ 𝑣 ≠ ∅))
2827simprbi 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣N𝑣 ≠ ∅)
2928neneqd 2241 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣N → ¬ 𝑣 = ∅)
3029ad2antll 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ¬ 𝑣 = ∅)
3126, 30jca 294 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → (¬ 𝑧 = ∅ ∧ ¬ 𝑣 = ∅))
32 pm4.56 817 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑧 = ∅ ∧ ¬ 𝑣 = ∅) ↔ ¬ (𝑧 = ∅ ∨ 𝑣 = ∅))
3331, 32sylib 131 . . . . . . . . . . . . . . . . . . . 20 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ¬ (𝑧 = ∅ ∨ 𝑣 = ∅))
34 pinn 6464 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧N𝑧 ∈ ω)
3534ad2antrr 465 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → 𝑧 ∈ ω)
36 pinn 6464 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣N𝑣 ∈ ω)
3736ad2antll 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → 𝑣 ∈ ω)
38 nnm00 6132 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ω ∧ 𝑣 ∈ ω) → ((𝑧 ·𝑜 𝑣) = ∅ ↔ (𝑧 = ∅ ∨ 𝑣 = ∅)))
3935, 37, 38syl2anc 397 . . . . . . . . . . . . . . . . . . . 20 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ((𝑧 ·𝑜 𝑣) = ∅ ↔ (𝑧 = ∅ ∨ 𝑣 = ∅)))
4033, 39mtbird 608 . . . . . . . . . . . . . . . . . . 19 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ¬ (𝑧 ·𝑜 𝑣) = ∅)
4140ad2ant2rl 488 . . . . . . . . . . . . . . . . . 18 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ¬ (𝑧 ·𝑜 𝑣) = ∅)
42 breq2 3795 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑢, 𝑣⟩ → (⟨𝑧, 𝑤⟩ ~Q0 𝑦 ↔ ⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩))
4342biimpac 286 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑧, 𝑤⟩ ~Q0 𝑦𝑦 = ⟨𝑢, 𝑣⟩) → ⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩)
4443ad2ant2lr 487 . . . . . . . . . . . . . . . . . . . 20 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩)
45 enq0breq 6591 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ω ∧ 𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → (⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩ ↔ (𝑧 ·𝑜 𝑣) = (𝑤 ·𝑜 𝑢)))
4634, 45sylanl1 388 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → (⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩ ↔ (𝑧 ·𝑜 𝑣) = (𝑤 ·𝑜 𝑢)))
4746ad2ant2rl 488 . . . . . . . . . . . . . . . . . . . 20 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → (⟨𝑧, 𝑤⟩ ~Q0𝑢, 𝑣⟩ ↔ (𝑧 ·𝑜 𝑣) = (𝑤 ·𝑜 𝑢)))
4844, 47mpbid 139 . . . . . . . . . . . . . . . . . . 19 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → (𝑧 ·𝑜 𝑣) = (𝑤 ·𝑜 𝑢))
4948eqeq1d 2064 . . . . . . . . . . . . . . . . . 18 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ((𝑧 ·𝑜 𝑣) = ∅ ↔ (𝑤 ·𝑜 𝑢) = ∅))
5041, 49mtbid 607 . . . . . . . . . . . . . . . . 17 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ¬ (𝑤 ·𝑜 𝑢) = ∅)
51 pinn 6464 . . . . . . . . . . . . . . . . . . . 20 (𝑤N𝑤 ∈ ω)
52 nnm00 6132 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ ω ∧ 𝑢 ∈ ω) → ((𝑤 ·𝑜 𝑢) = ∅ ↔ (𝑤 = ∅ ∨ 𝑢 = ∅)))
5351, 52sylan 271 . . . . . . . . . . . . . . . . . . 19 ((𝑤N𝑢 ∈ ω) → ((𝑤 ·𝑜 𝑢) = ∅ ↔ (𝑤 = ∅ ∨ 𝑢 = ∅)))
5453ad2ant2lr 487 . . . . . . . . . . . . . . . . . 18 (((𝑧N𝑤N) ∧ (𝑢 ∈ ω ∧ 𝑣N)) → ((𝑤 ·𝑜 𝑢) = ∅ ↔ (𝑤 = ∅ ∨ 𝑢 = ∅)))
5554ad2ant2rl 488 . . . . . . . . . . . . . . . . 17 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ((𝑤 ·𝑜 𝑢) = ∅ ↔ (𝑤 = ∅ ∨ 𝑢 = ∅)))
5650, 55mtbid 607 . . . . . . . . . . . . . . . 16 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ¬ (𝑤 = ∅ ∨ 𝑢 = ∅))
57 pm4.56 817 . . . . . . . . . . . . . . . 16 ((¬ 𝑤 = ∅ ∧ ¬ 𝑢 = ∅) ↔ ¬ (𝑤 = ∅ ∨ 𝑢 = ∅))
5856, 57sylibr 141 . . . . . . . . . . . . . . 15 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → (¬ 𝑤 = ∅ ∧ ¬ 𝑢 = ∅))
5958simprd 111 . . . . . . . . . . . . . 14 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → ¬ 𝑢 = ∅)
6059neneqad 2299 . . . . . . . . . . . . 13 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑢 ≠ ∅)
61 elni 6463 . . . . . . . . . . . . 13 (𝑢N ↔ (𝑢 ∈ ω ∧ 𝑢 ≠ ∅))
6222, 60, 61sylanbrc 402 . . . . . . . . . . . 12 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑢N)
63 simprrr 500 . . . . . . . . . . . 12 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑣N)
64 eleq1 2116 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑢, 𝑣⟩ → (𝑦 ∈ (N × N) ↔ ⟨𝑢, 𝑣⟩ ∈ (N × N)))
65 opelxp 4401 . . . . . . . . . . . . . 14 (⟨𝑢, 𝑣⟩ ∈ (N × N) ↔ (𝑢N𝑣N))
6664, 65syl6bb 189 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑢, 𝑣⟩ → (𝑦 ∈ (N × N) ↔ (𝑢N𝑣N)))
6766ad2antrl 467 . . . . . . . . . . . 12 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → (𝑦 ∈ (N × N) ↔ (𝑢N𝑣N)))
6862, 63, 67mpbir2and 862 . . . . . . . . . . 11 ((((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑦 ∈ (N × N))
6968exlimivv 1792 . . . . . . . . . 10 (∃𝑢𝑣(((𝑧N𝑤N) ∧ ⟨𝑧, 𝑤⟩ ~Q0 𝑦) ∧ (𝑦 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ ω ∧ 𝑣N))) → 𝑦 ∈ (N × N))
7021, 69syl 14 . . . . . . . . 9 (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) → 𝑦 ∈ (N × N))
7170exlimivv 1792 . . . . . . . 8 (∃𝑧𝑤((𝑥 = ⟨𝑧, 𝑤⟩ ∧ (𝑧N𝑤N)) ∧ 𝑥 ~Q0 𝑦) → 𝑦 ∈ (N × N))
727, 71sylbi 118 . . . . . . 7 ((𝑥 ∈ (N × N) ∧ 𝑥 ~Q0 𝑦) → 𝑦 ∈ (N × N))
7372exlimiv 1505 . . . . . 6 (∃𝑥(𝑥 ∈ (N × N) ∧ 𝑥 ~Q0 𝑦) → 𝑦 ∈ (N × N))
743, 73sylbi 118 . . . . 5 (𝑦 ∈ ( ~Q0 “ (N × N)) → 𝑦 ∈ (N × N))
7574ssriv 2976 . . . 4 ( ~Q0 “ (N × N)) ⊆ (N × N)
76 ecinxp 6211 . . . 4 ((( ~Q0 “ (N × N)) ⊆ (N × N) ∧ ⟨𝐴, 𝐵⟩ ∈ (N × N)) → [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩]( ~Q0 ∩ ((N × N) × (N × N))))
7775, 76mpan 408 . . 3 (⟨𝐴, 𝐵⟩ ∈ (N × N) → [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩]( ~Q0 ∩ ((N × N) × (N × N))))
781, 77sylbir 129 . 2 ((𝐴N𝐵N) → [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩]( ~Q0 ∩ ((N × N) × (N × N))))
79 enq0enq 6586 . . 3 ~Q = ( ~Q0 ∩ ((N × N) × (N × N)))
80 eceq2 6173 . . 3 ( ~Q = ( ~Q0 ∩ ((N × N) × (N × N))) → [⟨𝐴, 𝐵⟩] ~Q = [⟨𝐴, 𝐵⟩]( ~Q0 ∩ ((N × N) × (N × N))))
8179, 80ax-mp 7 . 2 [⟨𝐴, 𝐵⟩] ~Q = [⟨𝐴, 𝐵⟩]( ~Q0 ∩ ((N × N) × (N × N)))
8278, 81syl6eqr 2106 1 ((𝐴N𝐵N) → [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q )
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 101   ↔ wb 102   ∨ wo 639   = wceq 1259  ∃wex 1397   ∈ wcel 1409   ≠ wne 2220   ∩ cin 2943   ⊆ wss 2944  ∅c0 3251  ⟨cop 3405   class class class wbr 3791  ωcom 4340   × cxp 4370   “ cima 4375  (class class class)co 5539   ·𝑜 comu 6029   Er wer 6133  [cec 6134  Ncnpi 6427   ~Q ceq 6434   ~Q0 ceq0 6441 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338 This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-ov 5542  df-oprab 5543  df-mpt2 5544  df-1st 5794  df-2nd 5795  df-recs 5950  df-irdg 5987  df-oadd 6035  df-omul 6036  df-er 6136  df-ec 6138  df-ni 6459  df-mi 6461  df-enq 6502  df-enq0 6579 This theorem is referenced by:  nqnq0  6596  nqpnq0nq  6608  nqnq0a  6609  nqnq0m  6610  prarloclemlo  6649  prarloclemcalc  6657
 Copyright terms: Public domain W3C validator