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 39461
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 6676 . . . . 5 (𝑥 = 𝑦 → (2nd𝑥) = (2nd𝑦))
32eqeq1d 2740 . . . 4 (𝑥 = 𝑦 → ((2nd𝑥) = 0 ↔ (2nd𝑦) = 0 ))
42sneqd 4528 . . . . . . . . 9 (𝑥 = 𝑦 → {(2nd𝑥)} = {(2nd𝑦)})
54fveq2d 6680 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{(2nd𝑥)}) = (𝑁‘{(2nd𝑦)}))
65fveq2d 6680 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd𝑥)})) = (𝑀‘(𝑁‘{(2nd𝑦)})))
76eqeq1d 2740 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{})))
8 2fveq3 6681 . . . . . . . . . . 11 (𝑥 = 𝑦 → (1st ‘(1st𝑥)) = (1st ‘(1st𝑦)))
98, 2oveq12d 7190 . . . . . . . . . 10 (𝑥 = 𝑦 → ((1st ‘(1st𝑥)) (2nd𝑥)) = ((1st ‘(1st𝑦)) (2nd𝑦)))
109sneqd 4528 . . . . . . . . 9 (𝑥 = 𝑦 → {((1st ‘(1st𝑥)) (2nd𝑥))} = {((1st ‘(1st𝑦)) (2nd𝑦))})
1110fveq2d 6680 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))}) = (𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))}))
1211fveq2d 6680 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})))
13 2fveq3 6681 . . . . . . . . . 10 (𝑥 = 𝑦 → (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)))
1413oveq1d 7187 . . . . . . . . 9 (𝑥 = 𝑦 → ((2nd ‘(1st𝑥))𝑅) = ((2nd ‘(1st𝑦))𝑅))
1514sneqd 4528 . . . . . . . 8 (𝑥 = 𝑦 → {((2nd ‘(1st𝑥))𝑅)} = {((2nd ‘(1st𝑦))𝑅)})
1615fveq2d 6680 . . . . . . 7 (𝑥 = 𝑦 → (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))
1712, 16eqeq12d 2754 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))
187, 17anbi12d 634 . . . . 5 (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
1918riotabidv 7131 . . . 4 (𝑥 = 𝑦 → (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
203, 19ifbieq2d 4440 . . 3 (𝑥 = 𝑦 → if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
2120cbvmptv 5133 . 2 (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
22 sneq 4526 . . . . . . . 8 ( = 𝑖 → {} = {𝑖})
2322fveq2d 6680 . . . . . . 7 ( = 𝑖 → (𝐽‘{}) = (𝐽‘{𝑖}))
2423eqeq2d 2749 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖})))
25 oveq2 7180 . . . . . . . . 9 ( = 𝑖 → ((2nd ‘(1st𝑦))𝑅) = ((2nd ‘(1st𝑦))𝑅𝑖))
2625sneqd 4528 . . . . . . . 8 ( = 𝑖 → {((2nd ‘(1st𝑦))𝑅)} = {((2nd ‘(1st𝑦))𝑅𝑖)})
2726fveq2d 6680 . . . . . . 7 ( = 𝑖 → (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))
2827eqeq2d 2749 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
2924, 28anbi12d 634 . . . . 5 ( = 𝑖 → (((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3029cbvriotavw 7139 . . . 4 (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
31 ifeq2 4419 . . . 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 5122 . 2 (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
341, 21, 333eqtri 2765 1 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1542  Vcvv 3398  ifcif 4414  {csn 4516  cmpt 5110  cfv 6339  crio 7128  (class class class)co 7172  1st c1st 7714  2nd c2nd 7715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-iota 6297  df-fv 6347  df-riota 7129  df-ov 7175
This theorem is referenced by:  hdmap1valc  39462  hdmap1eu  39483  hdmap1euOLDN  39484
  Copyright terms: Public domain W3C validator