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

Theorem mpt2xopoveq 5777
 Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
Hypothesis
Ref Expression
mpt2xopoveq.f 𝐹 = (x V, y (1stx) ↦ {𝑛 (1stx) ∣ φ})
Assertion
Ref Expression
mpt2xopoveq (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → (⟨𝑉, 𝑊𝐹𝐾) = {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ})
Distinct variable groups:   𝑛,𝐾,x,y   𝑛,𝑉,x,y   𝑛,𝑊,x,y   𝑛,𝑋,x,y   𝑛,𝑌,x,y
Allowed substitution hints:   φ(x,y,𝑛)   𝐹(x,y,𝑛)

Proof of Theorem mpt2xopoveq
StepHypRef Expression
1 mpt2xopoveq.f . . 3 𝐹 = (x V, y (1stx) ↦ {𝑛 (1stx) ∣ φ})
21a1i 9 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → 𝐹 = (x V, y (1stx) ↦ {𝑛 (1stx) ∣ φ}))
3 fveq2 5103 . . . . 5 (x = ⟨𝑉, 𝑊⟩ → (1stx) = (1st ‘⟨𝑉, 𝑊⟩))
4 op1stg 5700 . . . . . 6 ((𝑉 𝑋 𝑊 𝑌) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
54adantr 261 . . . . 5 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
63, 5sylan9eqr 2076 . . . 4 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) x = ⟨𝑉, 𝑊⟩) → (1stx) = 𝑉)
76adantrr 451 . . 3 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → (1stx) = 𝑉)
8 sbceq1a 2750 . . . . . 6 (y = 𝐾 → (φ[𝐾 / y]φ))
98adantl 262 . . . . 5 ((x = ⟨𝑉, 𝑊 y = 𝐾) → (φ[𝐾 / y]φ))
109adantl 262 . . . 4 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → (φ[𝐾 / y]φ))
11 sbceq1a 2750 . . . . . 6 (x = ⟨𝑉, 𝑊⟩ → ([𝐾 / y]φ[𝑉, 𝑊⟩ / x][𝐾 / y]φ))
1211adantr 261 . . . . 5 ((x = ⟨𝑉, 𝑊 y = 𝐾) → ([𝐾 / y]φ[𝑉, 𝑊⟩ / x][𝐾 / y]φ))
1312adantl 262 . . . 4 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → ([𝐾 / y]φ[𝑉, 𝑊⟩ / x][𝐾 / y]φ))
1410, 13bitrd 177 . . 3 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → (φ[𝑉, 𝑊⟩ / x][𝐾 / y]φ))
157, 14rabeqbidv 2530 . 2 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → {𝑛 (1stx) ∣ φ} = {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ})
16 opexg 3938 . . 3 ((𝑉 𝑋 𝑊 𝑌) → ⟨𝑉, 𝑊 V)
1716adantr 261 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → ⟨𝑉, 𝑊 V)
18 simpr 103 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → 𝐾 𝑉)
19 rabexg 3874 . . 3 (𝑉 𝑋 → {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ} V)
2019ad2antrr 460 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ} V)
21 equid 1571 . . 3 z = z
22 nfvd 1403 . . 3 (z = z → Ⅎx((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉))
2321, 22ax-mp 7 . 2 x((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉)
24 nfvd 1403 . . 3 (z = z → Ⅎy((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉))
2521, 24ax-mp 7 . 2 y((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉)
26 nfcv 2160 . 2 y𝑉, 𝑊
27 nfcv 2160 . 2 x𝐾
28 nfsbc1v 2759 . . 3 x[𝑉, 𝑊⟩ / x][𝐾 / y]φ
29 nfcv 2160 . . 3 x𝑉
3028, 29nfrabxy 2468 . 2 x{𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ}
31 nfsbc1v 2759 . . . 4 y[𝐾 / y]φ
3226, 31nfsbc 2761 . . 3 y[𝑉, 𝑊⟩ / x][𝐾 / y]φ
33 nfcv 2160 . . 3 y𝑉
3432, 33nfrabxy 2468 . 2 y{𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ}
352, 15, 6, 17, 18, 20, 23, 25, 26, 27, 30, 34ovmpt2dxf 5549 1 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → (⟨𝑉, 𝑊𝐹𝐾) = {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ})
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1228  Ⅎwnf 1329   ∈ wcel 1374  {crab 2288  Vcvv 2535  [wsbc 2741  ⟨cop 3353  ‘cfv 4829  (class class class)co 5436   ↦ cmpt2 5438  1st c1st 5688 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204 This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-rab 2293  df-v 2537  df-sbc 2742  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-opab 3793  df-mpt 3794  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-iota 4794  df-fun 4831  df-fv 4837  df-ov 5439  df-oprab 5440  df-mpt2 5441  df-1st 5690 This theorem is referenced by:  mpt2xopovel  5778
 Copyright terms: Public domain W3C validator