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 ⊢ φ → ∃! h h : 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∈ V
8 5 6 7 3syl ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∈ V
9 feq1 ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h : A ⊔︀ B ⟶ C ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C
10 coeq1 ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h ∘ inl ↾ A = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A
11 10 eqeq1d ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h ∘ inl ↾ A = F ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F
12 coeq1 ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h ∘ inr ↾ B = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B
13 12 eqeq1d ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h ∘ inr ↾ B = G ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G
14 9 11 13 3anbi123d ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G
15 eqeq1 ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h = k ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
16 15 imbi2d ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
17 16 ralbidv ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → h = k ↔ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
18 14 17 anbi12d ⊢ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → h = k ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
19 18 adantl ⊢ φ ∧ h = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x → h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → h = k ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
20 eqid ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x
21 1 2 20 updjudhf ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C
22 1 2 20 updjudhcoinlf ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F
23 1 2 20 updjudhcoinrg ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G
24 simpr ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G
25 eqeq2 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F → k ∘ inl ↾ A = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → y = inl ⁡ z ↔ y = inl ↾ A ⁡ z
30 fveq1 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A ⁡ z = k ∘ inl ↾ A ⁡ z
31 30 ad2antrr ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A ⁡ z = k ∘ inl ↾ A ⁡ z
32 inlresf ⊢ inl ↾ A : A ⟶ A ⊔︀ B
33 ffn ⊢ inl ↾ A : A ⟶ A ⊔︀ B → inl ↾ A Fn A
34 32 33 mp1i ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ → inl ↾ A Fn A
35 fvco2 ⊢ inl ↾ A Fn A ∧ z ∈ A → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A ⁡ z = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inl ↾ A ⁡ z
36 34 35 sylan ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A ⁡ z = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inl ↾ A ⁡ z
37 fvco2 ⊢ inl ↾ A Fn A ∧ z ∈ A → k ∘ inl ↾ A ⁡ z = k ⁡ inl ↾ A ⁡ z
38 34 37 sylan ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → k ∘ inl ↾ A ⁡ z = k ⁡ inl ↾ A ⁡ z
39 31 36 38 3eqtr3d ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inl ↾ A ⁡ z = k ⁡ inl ↾ A ⁡ z
40 fveq2 ⊢ y = inl ↾ A ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inl ↾ A ⁡ z = k ⁡ inl ↾ A ⁡ z
43 39 42 syl5ibrcom ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → y = inl ↾ A ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
44 29 43 sylbid ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ ∧ z ∈ A → y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
45 44 expimpd ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A ∧ φ → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
46 45 ex ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = k ∘ inl ↾ A → φ → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
47 46 eqcoms ⊢ k ∘ inl ↾ A = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A → φ → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
48 25 47 syl6bir ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F → k ∘ inl ↾ A = F → φ → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
49 48 com23 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F → φ → k ∘ inl ↾ A = F → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
50 49 3ad2ant2 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → φ → k ∘ inl ↾ A = F → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
51 50 impcom ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → k ∘ inl ↾ A = F → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
52 51 com12 ⊢ k ∘ inl ↾ A = F → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
53 52 3ad2ant2 ⊢ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
54 53 impcom ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → z ∈ A ∧ y = inl ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
55 54 com12 ⊢ z ∈ A ∧ y = inl ⁡ z → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
56 55 rexlimiva ⊢ ∃ z ∈ A y = inl ⁡ z → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
57 eqeq2 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → k ∘ inr ↾ B = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → y = inr ⁡ z ↔ y = inr ↾ B ⁡ z
62 fveq1 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B ⁡ z = k ∘ inr ↾ B ⁡ z
63 62 ad2antrr ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B ⁡ z = k ∘ inr ↾ B ⁡ z
64 inrresf ⊢ inr ↾ B : B ⟶ A ⊔︀ B
65 ffn ⊢ inr ↾ B : B ⟶ A ⊔︀ B → inr ↾ B Fn B
66 64 65 mp1i ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ → inr ↾ B Fn B
67 fvco2 ⊢ inr ↾ B Fn B ∧ z ∈ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B ⁡ z = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inr ↾ B ⁡ z
68 66 67 sylan ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B ⁡ z = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inr ↾ B ⁡ z
69 fvco2 ⊢ inr ↾ B Fn B ∧ z ∈ B → k ∘ inr ↾ B ⁡ z = k ⁡ inr ↾ B ⁡ z
70 66 69 sylan ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → k ∘ inr ↾ B ⁡ z = k ⁡ inr ↾ B ⁡ z
71 63 68 70 3eqtr3d ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inr ↾ B ⁡ z = k ⁡ inr ↾ B ⁡ z
72 fveq2 ⊢ y = inr ↾ B ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ 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 ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y ↔ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ inr ↾ B ⁡ z = k ⁡ inr ↾ B ⁡ z
75 71 74 syl5ibrcom ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → y = inr ↾ B ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
76 61 75 sylbid ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ ∧ z ∈ B → y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
77 76 expimpd ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B ∧ φ → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
78 77 ex ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = k ∘ inr ↾ B → φ → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
79 78 eqcoms ⊢ k ∘ inr ↾ B = x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B → φ → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
80 57 79 syl6bir ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → k ∘ inr ↾ B = G → φ → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
81 80 com23 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → φ → k ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
82 81 3ad2ant3 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → φ → k ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
83 82 impcom ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → k ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
84 83 com12 ⊢ k ∘ inr ↾ B = G → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
85 84 3ad2ant3 ⊢ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
86 85 impcom ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → z ∈ B ∧ y = inr ⁡ z → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
87 86 com12 ⊢ z ∈ B ∧ y = inr ⁡ z → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
88 87 rexlimiva ⊢ ∃ z ∈ B y = inr ⁡ z → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
89 56 88 jaoi ⊢ ∃ z ∈ A y = inl ⁡ z ∨ ∃ z ∈ B y = inr ⁡ z → φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
90 djur ⊢ y ∈ A ⊔︀ B → ∃ z ∈ A y = inl ⁡ z ∨ ∃ z ∈ B y = inr ⁡ z
91 89 90 syl11 ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → y ∈ A ⊔︀ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
92 91 ralrimiv ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → ∀ y ∈ A ⊔︀ B x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
93 ffn ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x Fn A ⊔︀ B
94 93 3ad2ant1 ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x Fn A ⊔︀ B
95 94 adantl ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x Fn A ⊔︀ B
96 ffn ⊢ k : A ⊔︀ B ⟶ C → k Fn A ⊔︀ B
97 96 3ad2ant1 ⊢ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → k Fn A ⊔︀ B
98 eqfnfv ⊢ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x Fn A ⊔︀ B ∧ k Fn A ⊔︀ B → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k ↔ ∀ y ∈ A ⊔︀ B x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
99 95 97 98 syl2an ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k ↔ ∀ y ∈ A ⊔︀ B x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ⁡ y = k ⁡ y
100 92 99 mpbird ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
101 100 ex ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
102 101 ralrimivw ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
103 24 102 jca ⊢ φ ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
104 103 ex ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
105 21 22 23 104 mp3and ⊢ φ → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x : A ⊔︀ B ⟶ C ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inl ↾ A = F ∧ x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → x ∈ A ⊔︀ B ⟼ if 1 st ⁡ x = ∅ F ⁡ 2 nd ⁡ x G ⁡ 2 nd ⁡ x = k
106 8 19 105 rspcedvd ⊢ φ → ∃ h ∈ V h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ∧ ∀ k ∈ V k : 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 ∈ V h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ↔ ∃ h ∈ V h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ∧ ∀ k ∈ V k : A ⊔︀ B ⟶ C ∧ k ∘ inl ↾ A = F ∧ k ∘ inr ↾ B = G → h = k
114 106 113 sylibr ⊢ φ → ∃! h ∈ V h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G
115 reuv ⊢ ∃! h ∈ V h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G ↔ ∃! h h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G
116 114 115 sylib ⊢ φ → ∃! h h : A ⊔︀ B ⟶ C ∧ h ∘ inl ↾ A = F ∧ h ∘ inr ↾ B = G