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

Theorem ovmpt2df 5659
Description: Alternate deduction version of ovmpt2 5663, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
Hypotheses
Ref Expression
ovmpt2df.1 (𝜑𝐴𝐶)
ovmpt2df.2 ((𝜑𝑥 = 𝐴) → 𝐵𝐷)
ovmpt2df.3 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅𝑉)
ovmpt2df.4 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅𝜓))
ovmpt2df.5 𝑥𝐹
ovmpt2df.6 𝑥𝜓
ovmpt2df.7 𝑦𝐹
ovmpt2df.8 𝑦𝜓
Assertion
Ref Expression
ovmpt2df (𝜑 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ovmpt2df
StepHypRef Expression
1 nfv 1437 . 2 𝑥𝜑
2 ovmpt2df.5 . . . 4 𝑥𝐹
3 nfmpt21 5598 . . . 4 𝑥(𝑥𝐶, 𝑦𝐷𝑅)
42, 3nfeq 2201 . . 3 𝑥 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
5 ovmpt2df.6 . . 3 𝑥𝜓
64, 5nfim 1480 . 2 𝑥(𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓)
7 ovmpt2df.1 . . . 4 (𝜑𝐴𝐶)
8 elex 2583 . . . 4 (𝐴𝐶𝐴 ∈ V)
97, 8syl 14 . . 3 (𝜑𝐴 ∈ V)
10 isset 2578 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
119, 10sylib 131 . 2 (𝜑 → ∃𝑥 𝑥 = 𝐴)
12 ovmpt2df.2 . . . . 5 ((𝜑𝑥 = 𝐴) → 𝐵𝐷)
13 elex 2583 . . . . 5 (𝐵𝐷𝐵 ∈ V)
1412, 13syl 14 . . . 4 ((𝜑𝑥 = 𝐴) → 𝐵 ∈ V)
15 isset 2578 . . . 4 (𝐵 ∈ V ↔ ∃𝑦 𝑦 = 𝐵)
1614, 15sylib 131 . . 3 ((𝜑𝑥 = 𝐴) → ∃𝑦 𝑦 = 𝐵)
17 nfv 1437 . . . 4 𝑦(𝜑𝑥 = 𝐴)
18 ovmpt2df.7 . . . . . 6 𝑦𝐹
19 nfmpt22 5599 . . . . . 6 𝑦(𝑥𝐶, 𝑦𝐷𝑅)
2018, 19nfeq 2201 . . . . 5 𝑦 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
21 ovmpt2df.8 . . . . 5 𝑦𝜓
2220, 21nfim 1480 . . . 4 𝑦(𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓)
23 oveq 5545 . . . . . 6 (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → (𝐴𝐹𝐵) = (𝐴(𝑥𝐶, 𝑦𝐷𝑅)𝐵))
24 simprl 491 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑥 = 𝐴)
25 simprr 492 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑦 = 𝐵)
2624, 25oveq12d 5557 . . . . . . . . 9 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝑥(𝑥𝐶, 𝑦𝐷𝑅)𝑦) = (𝐴(𝑥𝐶, 𝑦𝐷𝑅)𝐵))
277adantr 265 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝐴𝐶)
2824, 27eqeltrd 2130 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑥𝐶)
2912adantrr 456 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝐵𝐷)
3025, 29eqeltrd 2130 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑦𝐷)
31 ovmpt2df.3 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅𝑉)
32 eqid 2056 . . . . . . . . . . 11 (𝑥𝐶, 𝑦𝐷𝑅) = (𝑥𝐶, 𝑦𝐷𝑅)
3332ovmpt4g 5650 . . . . . . . . . 10 ((𝑥𝐶𝑦𝐷𝑅𝑉) → (𝑥(𝑥𝐶, 𝑦𝐷𝑅)𝑦) = 𝑅)
3428, 30, 31, 33syl3anc 1146 . . . . . . . . 9 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝑥(𝑥𝐶, 𝑦𝐷𝑅)𝑦) = 𝑅)
3526, 34eqtr3d 2090 . . . . . . . 8 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝐴(𝑥𝐶, 𝑦𝐷𝑅)𝐵) = 𝑅)
3635eqeq2d 2067 . . . . . . 7 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥𝐶, 𝑦𝐷𝑅)𝐵) ↔ (𝐴𝐹𝐵) = 𝑅))
37 ovmpt2df.4 . . . . . . 7 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅𝜓))
3836, 37sylbid 143 . . . . . 6 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥𝐶, 𝑦𝐷𝑅)𝐵) → 𝜓))
3923, 38syl5 32 . . . . 5 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
4039expr 361 . . . 4 ((𝜑𝑥 = 𝐴) → (𝑦 = 𝐵 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓)))
4117, 22, 40exlimd 1504 . . 3 ((𝜑𝑥 = 𝐴) → (∃𝑦 𝑦 = 𝐵 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓)))
4216, 41mpd 13 . 2 ((𝜑𝑥 = 𝐴) → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
431, 6, 11, 42exlimdd 1768 1 (𝜑 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1259  wnf 1365  wex 1397  wcel 1409  wnfc 2181  Vcvv 2574  (class class class)co 5539  cmpt2 5541
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-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-setind 4289
This theorem depends on definitions:  df-bi 114  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-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-id 4057  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-iota 4894  df-fun 4931  df-fv 4937  df-ov 5542  df-oprab 5543  df-mpt2 5544
This theorem is referenced by:  ovmpt2dv  5660  ovmpt2dv2  5661
  Copyright terms: Public domain W3C validator