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 37613
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 6354 . . . . 5 (𝑥 = 𝑦 → (2nd𝑥) = (2nd𝑦))
32eqeq1d 2763 . . . 4 (𝑥 = 𝑦 → ((2nd𝑥) = 0 ↔ (2nd𝑦) = 0 ))
42sneqd 4334 . . . . . . . . 9 (𝑥 = 𝑦 → {(2nd𝑥)} = {(2nd𝑦)})
54fveq2d 6358 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{(2nd𝑥)}) = (𝑁‘{(2nd𝑦)}))
65fveq2d 6358 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd𝑥)})) = (𝑀‘(𝑁‘{(2nd𝑦)})))
76eqeq1d 2763 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{})))
8 fveq2 6354 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (1st𝑥) = (1st𝑦))
98fveq2d 6358 . . . . . . . . . . 11 (𝑥 = 𝑦 → (1st ‘(1st𝑥)) = (1st ‘(1st𝑦)))
109, 2oveq12d 6833 . . . . . . . . . 10 (𝑥 = 𝑦 → ((1st ‘(1st𝑥)) (2nd𝑥)) = ((1st ‘(1st𝑦)) (2nd𝑦)))
1110sneqd 4334 . . . . . . . . 9 (𝑥 = 𝑦 → {((1st ‘(1st𝑥)) (2nd𝑥))} = {((1st ‘(1st𝑦)) (2nd𝑦))})
1211fveq2d 6358 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))}) = (𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))}))
1312fveq2d 6358 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})))
148fveq2d 6358 . . . . . . . . . 10 (𝑥 = 𝑦 → (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)))
1514oveq1d 6830 . . . . . . . . 9 (𝑥 = 𝑦 → ((2nd ‘(1st𝑥))𝑅) = ((2nd ‘(1st𝑦))𝑅))
1615sneqd 4334 . . . . . . . 8 (𝑥 = 𝑦 → {((2nd ‘(1st𝑥))𝑅)} = {((2nd ‘(1st𝑦))𝑅)})
1716fveq2d 6358 . . . . . . 7 (𝑥 = 𝑦 → (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))
1813, 17eqeq12d 2776 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))
197, 18anbi12d 749 . . . . 5 (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
2019riotabidv 6778 . . . 4 (𝑥 = 𝑦 → (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
213, 20ifbieq2d 4256 . . 3 (𝑥 = 𝑦 → if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
2221cbvmptv 4903 . 2 (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
23 sneq 4332 . . . . . . . 8 ( = 𝑖 → {} = {𝑖})
2423fveq2d 6358 . . . . . . 7 ( = 𝑖 → (𝐽‘{}) = (𝐽‘{𝑖}))
2524eqeq2d 2771 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖})))
26 oveq2 6823 . . . . . . . . 9 ( = 𝑖 → ((2nd ‘(1st𝑦))𝑅) = ((2nd ‘(1st𝑦))𝑅𝑖))
2726sneqd 4334 . . . . . . . 8 ( = 𝑖 → {((2nd ‘(1st𝑦))𝑅)} = {((2nd ‘(1st𝑦))𝑅𝑖)})
2827fveq2d 6358 . . . . . . 7 ( = 𝑖 → (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))
2928eqeq2d 2771 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
3025, 29anbi12d 749 . . . . 5 ( = 𝑖 → (((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3130cbvriotav 6787 . . . 4 (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
32 ifeq2 4236 . . . 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𝑦))𝑅𝑖)})))))
3331, 32ax-mp 5 . . 3 if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3433mpteq2i 4894 . 2 (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
351, 22, 343eqtri 2787 1 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1632  Vcvv 3341  ifcif 4231  {csn 4322  cmpt 4882  cfv 6050  crio 6775  (class class class)co 6815  1st c1st 7333  2nd c2nd 7334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-iota 6013  df-fv 6058  df-riota 6776  df-ov 6818
This theorem is referenced by:  hdmap1valc  37614  hdmap1eu  37636  hdmap1euOLDN  37637
  Copyright terms: Public domain W3C validator