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

Theorem updjud 9351
Description: Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl 9319 and df-inr 9320, is the coproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct 9320 (25-Aug-2023). This is a special case of Example 1 of coproducts in Section 10.67 of [Adamek] p. 185. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
Hypotheses
Ref Expression
updjud.f (𝜑𝐹:𝐴𝐶)
updjud.g (𝜑𝐺:𝐵𝐶)
updjud.a (𝜑𝐴𝑉)
updjud.b (𝜑𝐵𝑊)
Assertion
Ref Expression
updjud (𝜑 → ∃!(:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))
Distinct variable groups:   𝐴,   𝐵,   𝐶,   ,𝐹   ,𝐺   𝜑,
Allowed substitution hints:   𝑉()   𝑊()

Proof of Theorem updjud
Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 updjud.a . . . . . 6 (𝜑𝐴𝑉)
2 updjud.b . . . . . 6 (𝜑𝐵𝑊)
31, 2jca 512 . . . . 5 (𝜑 → (𝐴𝑉𝐵𝑊))
4 djuex 9325 . . . . 5 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
5 mptexg 6975 . . . . 5 ((𝐴𝐵) ∈ V → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∈ V)
63, 4, 53syl 18 . . . 4 (𝜑 → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∈ V)
7 feq1 6488 . . . . . . 7 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (:(𝐴𝐵)⟶𝐶 ↔ (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶))
8 coeq1 5721 . . . . . . . 8 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → ( ∘ (inl ↾ 𝐴)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)))
98eqeq1d 2820 . . . . . . 7 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (( ∘ (inl ↾ 𝐴)) = 𝐹 ↔ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹))
10 coeq1 5721 . . . . . . . 8 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → ( ∘ (inr ↾ 𝐵)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)))
1110eqeq1d 2820 . . . . . . 7 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (( ∘ (inr ↾ 𝐵)) = 𝐺 ↔ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺))
127, 9, 113anbi123d 1427 . . . . . 6 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → ((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ↔ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)))
13 eqeq1 2822 . . . . . . . 8 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → ( = 𝑘 ↔ (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))
1413imbi2d 342 . . . . . . 7 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘) ↔ ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘)))
1514ralbidv 3194 . . . . . 6 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘) ↔ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘)))
1612, 15anbi12d 630 . . . . 5 ( = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) → (((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘)) ↔ (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))))
1716adantl 482 . . . 4 ((𝜑 = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))) → (((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘)) ↔ (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))))
18 updjud.f . . . . . 6 (𝜑𝐹:𝐴𝐶)
19 updjud.g . . . . . 6 (𝜑𝐺:𝐵𝐶)
20 eqid 2818 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))
2118, 19, 20updjudhf 9348 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶)
2218, 19, 20updjudhcoinlf 9349 . . . . 5 (𝜑 → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹)
2318, 19, 20updjudhcoinrg 9350 . . . . 5 (𝜑 → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)
24 simpr 485 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺))
25 eqeq2 2830 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝑘 ∘ (inl ↾ 𝐴)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) ↔ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹))
26 fvres 6682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝐴 → ((inl ↾ 𝐴)‘𝑧) = (inl‘𝑧))
2726eqcomd 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝐴 → (inl‘𝑧) = ((inl ↾ 𝐴)‘𝑧))
2827eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝐴 → (𝑦 = (inl‘𝑧) ↔ 𝑦 = ((inl ↾ 𝐴)‘𝑧)))
2928adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → (𝑦 = (inl‘𝑧) ↔ 𝑦 = ((inl ↾ 𝐴)‘𝑧)))
30 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴))‘𝑧) = ((𝑘 ∘ (inl ↾ 𝐴))‘𝑧))
3130ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴))‘𝑧) = ((𝑘 ∘ (inl ↾ 𝐴))‘𝑧))
32 inlresf 9331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (inl ↾ 𝐴):𝐴⟶(𝐴𝐵)
33 ffn 6507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((inl ↾ 𝐴):𝐴⟶(𝐴𝐵) → (inl ↾ 𝐴) Fn 𝐴)
3432, 33mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) → (inl ↾ 𝐴) Fn 𝐴)
35 fvco2 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((inl ↾ 𝐴) Fn 𝐴𝑧𝐴) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴))‘𝑧) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inl ↾ 𝐴)‘𝑧)))
3634, 35sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴))‘𝑧) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inl ↾ 𝐴)‘𝑧)))
37 fvco2 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((inl ↾ 𝐴) Fn 𝐴𝑧𝐴) → ((𝑘 ∘ (inl ↾ 𝐴))‘𝑧) = (𝑘‘((inl ↾ 𝐴)‘𝑧)))
3834, 37sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → ((𝑘 ∘ (inl ↾ 𝐴))‘𝑧) = (𝑘‘((inl ↾ 𝐴)‘𝑧)))
3931, 36, 383eqtr3d 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inl ↾ 𝐴)‘𝑧)) = (𝑘‘((inl ↾ 𝐴)‘𝑧)))
40 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ((inl ↾ 𝐴)‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inl ↾ 𝐴)‘𝑧)))
41 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ((inl ↾ 𝐴)‘𝑧) → (𝑘𝑦) = (𝑘‘((inl ↾ 𝐴)‘𝑧)))
4240, 41eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ((inl ↾ 𝐴)‘𝑧) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦) ↔ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inl ↾ 𝐴)‘𝑧)) = (𝑘‘((inl ↾ 𝐴)‘𝑧))))
4339, 42syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → (𝑦 = ((inl ↾ 𝐴)‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
4429, 43sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) ∧ 𝑧𝐴) → (𝑦 = (inl‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
4544expimpd 454 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) ∧ 𝜑) → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
4645ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)) → (𝜑 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
4746eqcoms 2826 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∘ (inl ↾ 𝐴)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) → (𝜑 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
4825, 47syl6bir 255 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 → (𝜑 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
4948com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 → (𝜑 → ((𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
50493ad2ant2 1126 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) → (𝜑 → ((𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
5150impcom 408 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
5251com12 32 . . . . . . . . . . . . . . . . 17 ((𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 → ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
53523ad2ant2 1126 . . . . . . . . . . . . . . . 16 ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
5453impcom 408 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐴𝑦 = (inl‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
5554com12 32 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = (inl‘𝑧)) → (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
5655rexlimiva 3278 . . . . . . . . . . . . 13 (∃𝑧𝐴 𝑦 = (inl‘𝑧) → (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
57 eqeq2 2830 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝑘 ∘ (inr ↾ 𝐵)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) ↔ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺))
58 fvres 6682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧𝐵 → ((inr ↾ 𝐵)‘𝑧) = (inr‘𝑧))
5958eqcomd 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝐵 → (inr‘𝑧) = ((inr ↾ 𝐵)‘𝑧))
6059eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝐵 → (𝑦 = (inr‘𝑧) ↔ 𝑦 = ((inr ↾ 𝐵)‘𝑧)))
6160adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → (𝑦 = (inr‘𝑧) ↔ 𝑦 = ((inr ↾ 𝐵)‘𝑧)))
62 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵))‘𝑧) = ((𝑘 ∘ (inr ↾ 𝐵))‘𝑧))
6362ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵))‘𝑧) = ((𝑘 ∘ (inr ↾ 𝐵))‘𝑧))
64 inrresf 9333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (inr ↾ 𝐵):𝐵⟶(𝐴𝐵)
65 ffn 6507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((inr ↾ 𝐵):𝐵⟶(𝐴𝐵) → (inr ↾ 𝐵) Fn 𝐵)
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) → (inr ↾ 𝐵) Fn 𝐵)
67 fvco2 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((inr ↾ 𝐵) Fn 𝐵𝑧𝐵) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵))‘𝑧) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inr ↾ 𝐵)‘𝑧)))
6866, 67sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵))‘𝑧) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inr ↾ 𝐵)‘𝑧)))
69 fvco2 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((inr ↾ 𝐵) Fn 𝐵𝑧𝐵) → ((𝑘 ∘ (inr ↾ 𝐵))‘𝑧) = (𝑘‘((inr ↾ 𝐵)‘𝑧)))
7066, 69sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → ((𝑘 ∘ (inr ↾ 𝐵))‘𝑧) = (𝑘‘((inr ↾ 𝐵)‘𝑧)))
7163, 68, 703eqtr3d 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inr ↾ 𝐵)‘𝑧)) = (𝑘‘((inr ↾ 𝐵)‘𝑧)))
72 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ((inr ↾ 𝐵)‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inr ↾ 𝐵)‘𝑧)))
73 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ((inr ↾ 𝐵)‘𝑧) → (𝑘𝑦) = (𝑘‘((inr ↾ 𝐵)‘𝑧)))
7472, 73eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ((inr ↾ 𝐵)‘𝑧) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦) ↔ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘((inr ↾ 𝐵)‘𝑧)) = (𝑘‘((inr ↾ 𝐵)‘𝑧))))
7571, 74syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → (𝑦 = ((inr ↾ 𝐵)‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
7661, 75sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) ∧ 𝑧𝐵) → (𝑦 = (inr‘𝑧) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
7776expimpd 454 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) ∧ 𝜑) → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
7877ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)) → (𝜑 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
7978eqcoms 2826 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∘ (inr ↾ 𝐵)) = ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) → (𝜑 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
8057, 79syl6bir 255 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝑘 ∘ (inr ↾ 𝐵)) = 𝐺 → (𝜑 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
8180com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺 → (𝜑 → ((𝑘 ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
82813ad2ant3 1127 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) → (𝜑 → ((𝑘 ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))))
8382impcom 408 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑘 ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
8483com12 32 . . . . . . . . . . . . . . . . 17 ((𝑘 ∘ (inr ↾ 𝐵)) = 𝐺 → ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
85843ad2ant3 1127 . . . . . . . . . . . . . . . 16 ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))))
8685impcom 408 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑧𝐵𝑦 = (inr‘𝑧)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
8786com12 32 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = (inr‘𝑧)) → (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
8887rexlimiva 3278 . . . . . . . . . . . . 13 (∃𝑧𝐵 𝑦 = (inr‘𝑧) → (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
8956, 88jaoi 851 . . . . . . . . . . . 12 ((∃𝑧𝐴 𝑦 = (inl‘𝑧) ∨ ∃𝑧𝐵 𝑦 = (inr‘𝑧)) → (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
90 djur 9336 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴𝐵) → (∃𝑧𝐴 𝑦 = (inl‘𝑧) ∨ ∃𝑧𝐵 𝑦 = (inr‘𝑧)))
9189, 90syl11 33 . . . . . . . . . . 11 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → (𝑦 ∈ (𝐴𝐵) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
9291ralrimiv 3178 . . . . . . . . . 10 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ∀𝑦 ∈ (𝐴𝐵)((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦))
93 ffn 6507 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) Fn (𝐴𝐵))
94933ad2ant1 1125 . . . . . . . . . . . 12 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) Fn (𝐴𝐵))
9594adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) Fn (𝐴𝐵))
96 ffn 6507 . . . . . . . . . . . 12 (𝑘:(𝐴𝐵)⟶𝐶𝑘 Fn (𝐴𝐵))
97963ad2ant1 1125 . . . . . . . . . . 11 ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → 𝑘 Fn (𝐴𝐵))
98 eqfnfv 6794 . . . . . . . . . . 11 (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) Fn (𝐴𝐵) ∧ 𝑘 Fn (𝐴𝐵)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘 ↔ ∀𝑦 ∈ (𝐴𝐵)((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
9995, 97, 98syl2an 595 . . . . . . . . . 10 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘 ↔ ∀𝑦 ∈ (𝐴𝐵)((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))‘𝑦) = (𝑘𝑦)))
10092, 99mpbird 258 . . . . . . . . 9 (((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) ∧ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘)
101100ex 413 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))
102101ralrimivw 3180 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))
10324, 102jca 512 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺)) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘)))
104103ex 413 . . . . 5 (𝜑 → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘))))
10521, 22, 23, 104mp3and 1455 . . . 4 (𝜑 → (((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))):(𝐴𝐵)⟶𝐶 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ((𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥)))) = 𝑘)))
1066, 17, 105rspcedvd 3623 . . 3 (𝜑 → ∃ ∈ V ((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘)))
107 feq1 6488 . . . . 5 ( = 𝑘 → (:(𝐴𝐵)⟶𝐶𝑘:(𝐴𝐵)⟶𝐶))
108 coeq1 5721 . . . . . 6 ( = 𝑘 → ( ∘ (inl ↾ 𝐴)) = (𝑘 ∘ (inl ↾ 𝐴)))
109108eqeq1d 2820 . . . . 5 ( = 𝑘 → (( ∘ (inl ↾ 𝐴)) = 𝐹 ↔ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹))
110 coeq1 5721 . . . . . 6 ( = 𝑘 → ( ∘ (inr ↾ 𝐵)) = (𝑘 ∘ (inr ↾ 𝐵)))
111110eqeq1d 2820 . . . . 5 ( = 𝑘 → (( ∘ (inr ↾ 𝐵)) = 𝐺 ↔ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺))
112107, 109, 1113anbi123d 1427 . . . 4 ( = 𝑘 → ((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ↔ (𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺)))
113112reu8 3721 . . 3 (∃! ∈ V (:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ↔ ∃ ∈ V ((:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ∧ ∀𝑘 ∈ V ((𝑘:(𝐴𝐵)⟶𝐶 ∧ (𝑘 ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (𝑘 ∘ (inr ↾ 𝐵)) = 𝐺) → = 𝑘)))
114106, 113sylibr 235 . 2 (𝜑 → ∃! ∈ V (:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))
115 reuv 3519 . 2 (∃! ∈ V (:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺) ↔ ∃!(:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))
116114, 115sylib 219 1 (𝜑 → ∃!(:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  ∃!weu 2646  wral 3135  wrex 3136  ∃!wreu 3137  Vcvv 3492  c0 4288  ifcif 4463  cmpt 5137  cres 5550  ccom 5552   Fn wfn 6343  wf 6344  cfv 6348  1st c1st 7676  2nd c2nd 7677  cdju 9315  inlcinl 9316  inrcinr 9317
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  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7570  df-1st 7678  df-2nd 7679  df-1o 8091  df-dju 9318  df-inl 9319  df-inr 9320
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator