Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hdmap1cbv Structured version   Visualization version   GIF version

Theorem hdmap1cbv 38818
Description: Frequently used lemma to change bound variables in 𝐿 hypothesis. (Contributed by NM, 15-May-2015.)
Hypothesis
Ref Expression
hdmap1cbv.l 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
Assertion
Ref Expression
hdmap1cbv 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Distinct variable groups:   ,𝑖,𝑥,𝑦,𝐷   ,𝐽,𝑖,𝑥,𝑦   ,𝑀,𝑖,𝑥,𝑦   ,𝑁,𝑖,𝑥,𝑦   𝑥, 0 ,𝑦   𝑥,𝑄,𝑦   𝑅,,𝑖,𝑥,𝑦   ,,𝑖,𝑥,𝑦
Allowed substitution hints:   𝑄(,𝑖)   𝐿(𝑥,𝑦,,𝑖)   0 (,𝑖)

Proof of Theorem hdmap1cbv
StepHypRef Expression
1 hdmap1cbv.l . 2 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
2 fveq2 6663 . . . . 5 (𝑥 = 𝑦 → (2nd𝑥) = (2nd𝑦))
32eqeq1d 2820 . . . 4 (𝑥 = 𝑦 → ((2nd𝑥) = 0 ↔ (2nd𝑦) = 0 ))
42sneqd 4569 . . . . . . . . 9 (𝑥 = 𝑦 → {(2nd𝑥)} = {(2nd𝑦)})
54fveq2d 6667 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{(2nd𝑥)}) = (𝑁‘{(2nd𝑦)}))
65fveq2d 6667 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd𝑥)})) = (𝑀‘(𝑁‘{(2nd𝑦)})))
76eqeq1d 2820 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{})))
8 2fveq3 6668 . . . . . . . . . . 11 (𝑥 = 𝑦 → (1st ‘(1st𝑥)) = (1st ‘(1st𝑦)))
98, 2oveq12d 7163 . . . . . . . . . 10 (𝑥 = 𝑦 → ((1st ‘(1st𝑥)) (2nd𝑥)) = ((1st ‘(1st𝑦)) (2nd𝑦)))
109sneqd 4569 . . . . . . . . 9 (𝑥 = 𝑦 → {((1st ‘(1st𝑥)) (2nd𝑥))} = {((1st ‘(1st𝑦)) (2nd𝑦))})
1110fveq2d 6667 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))}) = (𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))}))
1211fveq2d 6667 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})))
13 2fveq3 6668 . . . . . . . . . 10 (𝑥 = 𝑦 → (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)))
1413oveq1d 7160 . . . . . . . . 9 (𝑥 = 𝑦 → ((2nd ‘(1st𝑥))𝑅) = ((2nd ‘(1st𝑦))𝑅))
1514sneqd 4569 . . . . . . . 8 (𝑥 = 𝑦 → {((2nd ‘(1st𝑥))𝑅)} = {((2nd ‘(1st𝑦))𝑅)})
1615fveq2d 6667 . . . . . . 7 (𝑥 = 𝑦 → (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))
1712, 16eqeq12d 2834 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))
187, 17anbi12d 630 . . . . 5 (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
1918riotabidv 7105 . . . 4 (𝑥 = 𝑦 → (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
203, 19ifbieq2d 4488 . . 3 (𝑥 = 𝑦 → if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
2120cbvmptv 5160 . 2 (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
22 sneq 4567 . . . . . . . 8 ( = 𝑖 → {} = {𝑖})
2322fveq2d 6667 . . . . . . 7 ( = 𝑖 → (𝐽‘{}) = (𝐽‘{𝑖}))
2423eqeq2d 2829 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖})))
25 oveq2 7153 . . . . . . . . 9 ( = 𝑖 → ((2nd ‘(1st𝑦))𝑅) = ((2nd ‘(1st𝑦))𝑅𝑖))
2625sneqd 4569 . . . . . . . 8 ( = 𝑖 → {((2nd ‘(1st𝑦))𝑅)} = {((2nd ‘(1st𝑦))𝑅𝑖)})
2726fveq2d 6667 . . . . . . 7 ( = 𝑖 → (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))
2827eqeq2d 2829 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
2924, 28anbi12d 630 . . . . 5 ( = 𝑖 → (((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3029cbvriotavw 7113 . . . 4 (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
31 ifeq2 4468 . . . 4 ((𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))) → if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
3230, 31ax-mp 5 . . 3 if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3332mpteq2i 5149 . 2 (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
341, 21, 333eqtri 2845 1 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  Vcvv 3492  ifcif 4463  {csn 4557  cmpt 5137  cfv 6348  crio 7102  (class class class)co 7145  1st c1st 7676  2nd c2nd 7677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-iota 6307  df-fv 6356  df-riota 7103  df-ov 7148
This theorem is referenced by:  hdmap1valc  38819  hdmap1eu  38840  hdmap1euOLDN  38841
  Copyright terms: Public domain W3C validator