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

 Description: Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 7064. (Contributed by Jim Kingdon, 14-Jul-2021.)
Assertion
Ref Expression
addvalex ((𝐴𝑉𝐵𝑊) → (𝐴 + 𝐵) ∈ V)

Dummy variables 𝑢 𝑓 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 5543 . 2 (𝐴 + 𝐵) = ( + ‘⟨𝐴, 𝐵⟩)
2 df-nr 6870 . . . . 5 R = ((P × P) / ~R )
3 npex 6629 . . . . . . 7 P ∈ V
43, 3xpex 4481 . . . . . 6 (P × P) ∈ V
54qsex 6194 . . . . 5 ((P × P) / ~R ) ∈ V
62, 5eqeltri 2126 . . . 4 R ∈ V
7 df-add 6958 . . . . 5 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
8 df-c 6953 . . . . . . . . 9 ℂ = (R × R)
98eleq2i 2120 . . . . . . . 8 (𝑥 ∈ ℂ ↔ 𝑥 ∈ (R × R))
108eleq2i 2120 . . . . . . . 8 (𝑦 ∈ ℂ ↔ 𝑦 ∈ (R × R))
119, 10anbi12i 441 . . . . . . 7 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ↔ (𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)))
1211anbi1i 439 . . . . . 6 (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)) ↔ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩)))
1312oprabbii 5588 . . . . 5 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
147, 13eqtri 2076 . . . 4 + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
156, 14oprabex3 5784 . . 3 + ∈ V
16 opexg 3992 . . 3 ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)
17 fvexg 5222 . . 3 (( + ∈ V ∧ ⟨𝐴, 𝐵⟩ ∈ V) → ( + ‘⟨𝐴, 𝐵⟩) ∈ V)
1815, 16, 17sylancr 399 . 2 ((𝐴𝑉𝐵𝑊) → ( + ‘⟨𝐴, 𝐵⟩) ∈ V)
191, 18syl5eqel 2140 1 ((𝐴𝑉𝐵𝑊) → (𝐴 + 𝐵) ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   = wceq 1259  ∃wex 1397   ∈ wcel 1409  Vcvv 2574  ⟨cop 3406   × cxp 4371  ‘cfv 4930  (class class class)co 5540  {coprab 5541   / cqs 6136  Pcnp 6447   ~R cer 6452  Rcnr 6453   +R cplr 6457  ℂcc 6945   + caddc 6950 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 3900  ax-sep 3903  ax-pow 3955  ax-pr 3972  ax-un 4198  ax-iinf 4339 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  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-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2788  df-csb 2881  df-dif 2948  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-int 3644  df-iun 3687  df-br 3793  df-opab 3847  df-mpt 3848  df-id 4058  df-iom 4342  df-xp 4379  df-rel 4380  df-cnv 4381  df-co 4382  df-dm 4383  df-rn 4384  df-res 4385  df-ima 4386  df-iota 4895  df-fun 4932  df-fn 4933  df-f 4934  df-f1 4935  df-fo 4936  df-f1o 4937  df-fv 4938  df-ov 5543  df-oprab 5544  df-qs 6143  df-ni 6460  df-nqqs 6504  df-inp 6622  df-nr 6870  df-c 6953  df-add 6958 This theorem is referenced by:  peano2nnnn  6987
 Copyright terms: Public domain W3C validator