MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  updjudhcoinlf Structured version   Visualization version   GIF version

Theorem updjudhcoinlf 9930
Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
Hypotheses
Ref Expression
updjud.f (πœ‘ β†’ 𝐹:𝐴⟢𝐢)
updjud.g (πœ‘ β†’ 𝐺:𝐡⟢𝐢)
updjudhf.h 𝐻 = (π‘₯ ∈ (𝐴 βŠ” 𝐡) ↦ if((1st β€˜π‘₯) = βˆ…, (πΉβ€˜(2nd β€˜π‘₯)), (πΊβ€˜(2nd β€˜π‘₯))))
Assertion
Ref Expression
updjudhcoinlf (πœ‘ β†’ (𝐻 ∘ (inl β†Ύ 𝐴)) = 𝐹)
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐢   πœ‘,π‘₯   π‘₯,𝐹
Allowed substitution hints:   𝐺(π‘₯)   𝐻(π‘₯)

Proof of Theorem updjudhcoinlf
Dummy variable π‘Ž is distinct from all other variables.
StepHypRef Expression
1 updjud.f . . . . 5 (πœ‘ β†’ 𝐹:𝐴⟢𝐢)
2 updjud.g . . . . 5 (πœ‘ β†’ 𝐺:𝐡⟢𝐢)
3 updjudhf.h . . . . 5 𝐻 = (π‘₯ ∈ (𝐴 βŠ” 𝐡) ↦ if((1st β€˜π‘₯) = βˆ…, (πΉβ€˜(2nd β€˜π‘₯)), (πΊβ€˜(2nd β€˜π‘₯))))
41, 2, 3updjudhf 9929 . . . 4 (πœ‘ β†’ 𝐻:(𝐴 βŠ” 𝐡)⟢𝐢)
54ffnd 6719 . . 3 (πœ‘ β†’ 𝐻 Fn (𝐴 βŠ” 𝐡))
6 inlresf 9912 . . . 4 (inl β†Ύ 𝐴):𝐴⟢(𝐴 βŠ” 𝐡)
7 ffn 6718 . . . 4 ((inl β†Ύ 𝐴):𝐴⟢(𝐴 βŠ” 𝐡) β†’ (inl β†Ύ 𝐴) Fn 𝐴)
86, 7mp1i 13 . . 3 (πœ‘ β†’ (inl β†Ύ 𝐴) Fn 𝐴)
9 frn 6725 . . . 4 ((inl β†Ύ 𝐴):𝐴⟢(𝐴 βŠ” 𝐡) β†’ ran (inl β†Ύ 𝐴) βŠ† (𝐴 βŠ” 𝐡))
106, 9mp1i 13 . . 3 (πœ‘ β†’ ran (inl β†Ύ 𝐴) βŠ† (𝐴 βŠ” 𝐡))
11 fnco 6668 . . 3 ((𝐻 Fn (𝐴 βŠ” 𝐡) ∧ (inl β†Ύ 𝐴) Fn 𝐴 ∧ ran (inl β†Ύ 𝐴) βŠ† (𝐴 βŠ” 𝐡)) β†’ (𝐻 ∘ (inl β†Ύ 𝐴)) Fn 𝐴)
125, 8, 10, 11syl3anc 1370 . 2 (πœ‘ β†’ (𝐻 ∘ (inl β†Ύ 𝐴)) Fn 𝐴)
131ffnd 6719 . 2 (πœ‘ β†’ 𝐹 Fn 𝐴)
14 fvco2 6989 . . . 4 (((inl β†Ύ 𝐴) Fn 𝐴 ∧ π‘Ž ∈ 𝐴) β†’ ((𝐻 ∘ (inl β†Ύ 𝐴))β€˜π‘Ž) = (π»β€˜((inl β†Ύ 𝐴)β€˜π‘Ž)))
158, 14sylan 579 . . 3 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((𝐻 ∘ (inl β†Ύ 𝐴))β€˜π‘Ž) = (π»β€˜((inl β†Ύ 𝐴)β€˜π‘Ž)))
16 fvres 6911 . . . . . 6 (π‘Ž ∈ 𝐴 β†’ ((inl β†Ύ 𝐴)β€˜π‘Ž) = (inlβ€˜π‘Ž))
1716adantl 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((inl β†Ύ 𝐴)β€˜π‘Ž) = (inlβ€˜π‘Ž))
1817fveq2d 6896 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π»β€˜((inl β†Ύ 𝐴)β€˜π‘Ž)) = (π»β€˜(inlβ€˜π‘Ž)))
19 fveqeq2 6901 . . . . . . . 8 (π‘₯ = (inlβ€˜π‘Ž) β†’ ((1st β€˜π‘₯) = βˆ… ↔ (1st β€˜(inlβ€˜π‘Ž)) = βˆ…))
20 2fveq3 6897 . . . . . . . 8 (π‘₯ = (inlβ€˜π‘Ž) β†’ (πΉβ€˜(2nd β€˜π‘₯)) = (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
21 2fveq3 6897 . . . . . . . 8 (π‘₯ = (inlβ€˜π‘Ž) β†’ (πΊβ€˜(2nd β€˜π‘₯)) = (πΊβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
2219, 20, 21ifbieq12d 4557 . . . . . . 7 (π‘₯ = (inlβ€˜π‘Ž) β†’ if((1st β€˜π‘₯) = βˆ…, (πΉβ€˜(2nd β€˜π‘₯)), (πΊβ€˜(2nd β€˜π‘₯))) = if((1st β€˜(inlβ€˜π‘Ž)) = βˆ…, (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))), (πΊβ€˜(2nd β€˜(inlβ€˜π‘Ž)))))
2322adantl 481 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ = (inlβ€˜π‘Ž)) β†’ if((1st β€˜π‘₯) = βˆ…, (πΉβ€˜(2nd β€˜π‘₯)), (πΊβ€˜(2nd β€˜π‘₯))) = if((1st β€˜(inlβ€˜π‘Ž)) = βˆ…, (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))), (πΊβ€˜(2nd β€˜(inlβ€˜π‘Ž)))))
24 1stinl 9925 . . . . . . . . 9 (π‘Ž ∈ 𝐴 β†’ (1st β€˜(inlβ€˜π‘Ž)) = βˆ…)
2524adantl 481 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (1st β€˜(inlβ€˜π‘Ž)) = βˆ…)
2625adantr 480 . . . . . . 7 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ = (inlβ€˜π‘Ž)) β†’ (1st β€˜(inlβ€˜π‘Ž)) = βˆ…)
2726iftrued 4537 . . . . . 6 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ = (inlβ€˜π‘Ž)) β†’ if((1st β€˜(inlβ€˜π‘Ž)) = βˆ…, (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))), (πΊβ€˜(2nd β€˜(inlβ€˜π‘Ž)))) = (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
2823, 27eqtrd 2771 . . . . 5 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ π‘₯ = (inlβ€˜π‘Ž)) β†’ if((1st β€˜π‘₯) = βˆ…, (πΉβ€˜(2nd β€˜π‘₯)), (πΊβ€˜(2nd β€˜π‘₯))) = (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
29 djulcl 9908 . . . . . 6 (π‘Ž ∈ 𝐴 β†’ (inlβ€˜π‘Ž) ∈ (𝐴 βŠ” 𝐡))
3029adantl 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (inlβ€˜π‘Ž) ∈ (𝐴 βŠ” 𝐡))
311adantr 480 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ 𝐹:𝐴⟢𝐢)
32 2ndinl 9926 . . . . . . . 8 (π‘Ž ∈ 𝐴 β†’ (2nd β€˜(inlβ€˜π‘Ž)) = π‘Ž)
3332adantl 481 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (2nd β€˜(inlβ€˜π‘Ž)) = π‘Ž)
34 simpr 484 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ 𝐴)
3533, 34eqeltrd 2832 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (2nd β€˜(inlβ€˜π‘Ž)) ∈ 𝐴)
3631, 35ffvelcdmd 7088 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))) ∈ 𝐢)
373, 28, 30, 36fvmptd2 7007 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π»β€˜(inlβ€˜π‘Ž)) = (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
3818, 37eqtrd 2771 . . 3 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π»β€˜((inl β†Ύ 𝐴)β€˜π‘Ž)) = (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))))
3933fveq2d 6896 . . 3 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (πΉβ€˜(2nd β€˜(inlβ€˜π‘Ž))) = (πΉβ€˜π‘Ž))
4015, 38, 393eqtrd 2775 . 2 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((𝐻 ∘ (inl β†Ύ 𝐴))β€˜π‘Ž) = (πΉβ€˜π‘Ž))
4112, 13, 40eqfnfvd 7036 1 (πœ‘ β†’ (𝐻 ∘ (inl β†Ύ 𝐴)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529   ↦ cmpt 5232  ran crn 5678   β†Ύ cres 5679   ∘ ccom 5681   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  1st c1st 7976  2nd c2nd 7977   βŠ” cdju 9896  inlcinl 9897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-1st 7978  df-2nd 7979  df-1o 8469  df-dju 9899  df-inl 9900
This theorem is referenced by:  updjud  9932
  Copyright terms: Public domain W3C validator