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

Theorem mpt2xopoveq 5796
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 5121 . . . . 5 (x = ⟨𝑉, 𝑊⟩ → (1stx) = (1st ‘⟨𝑉, 𝑊⟩))
4 op1stg 5719 . . . . . 6 ((𝑉 𝑋 𝑊 𝑌) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
54adantr 261 . . . . 5 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
63, 5sylan9eqr 2091 . . . 4 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) x = ⟨𝑉, 𝑊⟩) → (1stx) = 𝑉)
76adantrr 448 . . 3 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → (1stx) = 𝑉)
8 sbceq1a 2767 . . . . . 6 (y = 𝐾 → (φ[𝐾 / y]φ))
98adantl 262 . . . . 5 ((x = ⟨𝑉, 𝑊 y = 𝐾) → (φ[𝐾 / y]φ))
109adantl 262 . . . 4 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → (φ[𝐾 / y]φ))
11 sbceq1a 2767 . . . . . 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 2546 . 2 ((((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) (x = ⟨𝑉, 𝑊 y = 𝐾)) → {𝑛 (1stx) ∣ φ} = {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ})
16 opexg 3955 . . 3 ((𝑉 𝑋 𝑊 𝑌) → ⟨𝑉, 𝑊 V)
1716adantr 261 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → ⟨𝑉, 𝑊 V)
18 simpr 103 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → 𝐾 𝑉)
19 rabexg 3891 . . 3 (𝑉 𝑋 → {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ} V)
2019ad2antrr 457 . 2 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ} V)
21 equid 1586 . . 3 z = z
22 nfvd 1419 . . 3 (z = z → Ⅎx((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉))
2321, 22ax-mp 7 . 2 x((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉)
24 nfvd 1419 . . 3 (z = z → Ⅎy((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉))
2521, 24ax-mp 7 . 2 y((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉)
26 nfcv 2175 . 2 y𝑉, 𝑊
27 nfcv 2175 . 2 x𝐾
28 nfsbc1v 2776 . . 3 x[𝑉, 𝑊⟩ / x][𝐾 / y]φ
29 nfcv 2175 . . 3 x𝑉
3028, 29nfrabxy 2484 . 2 x{𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ}
31 nfsbc1v 2776 . . . 4 y[𝐾 / y]φ
3226, 31nfsbc 2778 . . 3 y[𝑉, 𝑊⟩ / x][𝐾 / y]φ
33 nfcv 2175 . . 3 y𝑉
3432, 33nfrabxy 2484 . 2 y{𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ}
352, 15, 6, 17, 18, 20, 23, 25, 26, 27, 30, 34ovmpt2dxf 5568 1 (((𝑉 𝑋 𝑊 𝑌) 𝐾 𝑉) → (⟨𝑉, 𝑊𝐹𝐾) = {𝑛 𝑉[𝑉, 𝑊⟩ / x][𝐾 / y]φ})
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242  wnf 1346   wcel 1390  {crab 2304  Vcvv 2551  [wsbc 2758  cop 3370  cfv 4845  (class class class)co 5455  cmpt2 5457  1st c1st 5707
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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709
This theorem is referenced by:  mpt2xopovel  5797
  Copyright terms: Public domain W3C validator