Metamath Proof Explorer

Theorem updjud

Description: Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl and df-inr , is thecoproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct (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)

Ref Expression
Hypotheses updjud.f ⊢φ→F:A⟶C
updjud.g ⊢φ→G:B⟶C
updjud.a ⊢φ→A∈V
updjud.b ⊢φ→B∈W
Assertion updjud ⊢φ→∃!hh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G

Proof

Step Hyp Ref Expression
1 updjud.f ⊢φ→F:A⟶C
2 updjud.g ⊢φ→G:B⟶C
3 updjud.a ⊢φ→A∈V
4 updjud.b ⊢φ→B∈W
5 3 4 jca ⊢φ→A∈V∧B∈W
6 djuex ⊢A∈V∧B∈W→A⊔︀B∈V
7 mptexg ⊢A⊔︀B∈V→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∈V
8 5 6 7 3syl ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∈V
9 feq1 ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h:A⊔︀B⟶C↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C
10 coeq1 ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h∘inl↾A=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A
11 10 eqeq1d ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h∘inl↾A=F↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F
12 coeq1 ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h∘inr↾B=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B
13 12 eqeq1d ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h∘inr↾B=G↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G
14 9 11 13 3anbi123d ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G
15 eqeq1 ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h=k↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
16 15 imbi2d ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k↔k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
17 16 ralbidv ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k↔∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
18 14 17 anbi12d ⊢h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
19 18 adantl ⊢φ∧h=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x→h:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
20 eqid ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x
21 1 2 20 updjudhf ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C
22 1 2 20 updjudhcoinlf ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F
23 1 2 20 updjudhcoinrg ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G
24 simpr ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G
25 eqeq2 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F→k∘inl↾A=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A↔k∘inl↾A=F
26 fvres ⊢z∈A→inl↾A⁡z=inl⁡z
27 26 eqcomd ⊢z∈A→inl⁡z=inl↾A⁡z
28 27 eqeq2d ⊢z∈A→y=inl⁡z↔y=inl↾A⁡z
29 28 adantl ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→y=inl⁡z↔y=inl↾A⁡z
30 fveq1 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A⁡z=k∘inl↾A⁡z
31 30 ad2antrr ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A⁡z=k∘inl↾A⁡z
32 inlresf ⊢inl↾A:A⟶A⊔︀B
33 ffn ⊢inl↾A:A⟶A⊔︀B→inl↾AFnA
34 32 33 mp1i ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ→inl↾AFnA
35 fvco2 ⊢inl↾AFnA∧z∈A→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A⁡z=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inl↾A⁡z
36 34 35 sylan ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A⁡z=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inl↾A⁡z
37 fvco2 ⊢inl↾AFnA∧z∈A→k∘inl↾A⁡z=k⁡inl↾A⁡z
38 34 37 sylan ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→k∘inl↾A⁡z=k⁡inl↾A⁡z
39 31 36 38 3eqtr3d ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inl↾A⁡z=k⁡inl↾A⁡z
40 fveq2 ⊢y=inl↾A⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inl↾A⁡z
41 fveq2 ⊢y=inl↾A⁡z→k⁡y=k⁡inl↾A⁡z
42 40 41 eqeq12d ⊢y=inl↾A⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inl↾A⁡z=k⁡inl↾A⁡z
43 39 42 syl5ibrcom ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→y=inl↾A⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
44 29 43 sylbid ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ∧z∈A→y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
45 44 expimpd ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A∧φ→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
46 45 ex ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=k∘inl↾A→φ→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
47 46 eqcoms ⊢k∘inl↾A=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A→φ→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
48 25 47 syl6bir ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F→k∘inl↾A=F→φ→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
49 48 com23 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F→φ→k∘inl↾A=F→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
50 49 3ad2ant2 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→φ→k∘inl↾A=F→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
51 50 impcom ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→k∘inl↾A=F→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
52 51 com12 ⊢k∘inl↾A=F→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
53 52 3ad2ant2 ⊢k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
54 53 impcom ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→z∈A∧y=inl⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
55 54 com12 ⊢z∈A∧y=inl⁡z→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
56 55 rexlimiva ⊢∃z∈Ay=inl⁡z→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
57 eqeq2 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→k∘inr↾B=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B↔k∘inr↾B=G
58 fvres ⊢z∈B→inr↾B⁡z=inr⁡z
59 58 eqcomd ⊢z∈B→inr⁡z=inr↾B⁡z
60 59 eqeq2d ⊢z∈B→y=inr⁡z↔y=inr↾B⁡z
61 60 adantl ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→y=inr⁡z↔y=inr↾B⁡z
62 fveq1 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B⁡z=k∘inr↾B⁡z
63 62 ad2antrr ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B⁡z=k∘inr↾B⁡z
64 inrresf ⊢inr↾B:B⟶A⊔︀B
65 ffn ⊢inr↾B:B⟶A⊔︀B→inr↾BFnB
66 64 65 mp1i ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ→inr↾BFnB
67 fvco2 ⊢inr↾BFnB∧z∈B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B⁡z=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inr↾B⁡z
68 66 67 sylan ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B⁡z=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inr↾B⁡z
69 fvco2 ⊢inr↾BFnB∧z∈B→k∘inr↾B⁡z=k⁡inr↾B⁡z
70 66 69 sylan ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→k∘inr↾B⁡z=k⁡inr↾B⁡z
71 63 68 70 3eqtr3d ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inr↾B⁡z=k⁡inr↾B⁡z
72 fveq2 ⊢y=inr↾B⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inr↾B⁡z
73 fveq2 ⊢y=inr↾B⁡z→k⁡y=k⁡inr↾B⁡z
74 72 73 eqeq12d ⊢y=inr↾B⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y↔x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡inr↾B⁡z=k⁡inr↾B⁡z
75 71 74 syl5ibrcom ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→y=inr↾B⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
76 61 75 sylbid ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ∧z∈B→y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
77 76 expimpd ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B∧φ→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
78 77 ex ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=k∘inr↾B→φ→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
79 78 eqcoms ⊢k∘inr↾B=x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B→φ→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
80 57 79 syl6bir ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→k∘inr↾B=G→φ→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
81 80 com23 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→φ→k∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
82 81 3ad2ant3 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→φ→k∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
83 82 impcom ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→k∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
84 83 com12 ⊢k∘inr↾B=G→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
85 84 3ad2ant3 ⊢k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
86 85 impcom ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→z∈B∧y=inr⁡z→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
87 86 com12 ⊢z∈B∧y=inr⁡z→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
88 87 rexlimiva ⊢∃z∈By=inr⁡z→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
89 56 88 jaoi ⊢∃z∈Ay=inl⁡z∨∃z∈By=inr⁡z→φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
90 djur ⊢y∈A⊔︀B→∃z∈Ay=inl⁡z∨∃z∈By=inr⁡z
91 89 90 syl11 ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→y∈A⊔︀B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
92 91 ralrimiv ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→∀y∈A⊔︀Bx∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
93 ffn ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡xFnA⊔︀B
94 93 3ad2ant1 ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡xFnA⊔︀B
95 94 adantl ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡xFnA⊔︀B
96 ffn ⊢k:A⊔︀B⟶C→kFnA⊔︀B
97 96 3ad2ant1 ⊢k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→kFnA⊔︀B
98 eqfnfv ⊢x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡xFnA⊔︀B∧kFnA⊔︀B→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k↔∀y∈A⊔︀Bx∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
99 95 97 98 syl2an ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k↔∀y∈A⊔︀Bx∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x⁡y=k⁡y
100 92 99 mpbird ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
101 100 ex ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
102 101 ralrimivw ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
103 24 102 jca ⊢φ∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
104 103 ex ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
105 21 22 23 104 mp3and ⊢φ→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x:A⊔︀B⟶C∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inl↾A=F∧x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→x∈A⊔︀B⟼if1st⁡x=∅F⁡2nd⁡xG⁡2nd⁡x=k
106 8 19 105 rspcedvd ⊢φ→∃h∈Vh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k
107 feq1 ⊢h=k→h:A⊔︀B⟶C↔k:A⊔︀B⟶C
108 coeq1 ⊢h=k→h∘inl↾A=k∘inl↾A
109 108 eqeq1d ⊢h=k→h∘inl↾A=F↔k∘inl↾A=F
110 coeq1 ⊢h=k→h∘inr↾B=k∘inr↾B
111 110 eqeq1d ⊢h=k→h∘inr↾B=G↔k∘inr↾B=G
112 107 109 111 3anbi123d ⊢h=k→h:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G↔k:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G
113 112 reu8 ⊢∃!h∈Vh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G↔∃h∈Vh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G∧∀k∈Vk:A⊔︀B⟶C∧k∘inl↾A=F∧k∘inr↾B=G→h=k
114 106 113 sylibr ⊢φ→∃!h∈Vh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G
115 reuv ⊢∃!h∈Vh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G↔∃!hh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G
116 114 115 sylib ⊢φ→∃!hh:A⊔︀B⟶C∧h∘inl↾A=F∧h∘inr↾B=G