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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
updjud.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
updjud.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
updjud.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion updjud ( 𝜑 → ∃! ℎ ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 updjud.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
2 updjud.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
3 updjud.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 updjud.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5 3 4 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
6 djuex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )
7 mptexg ⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∈ V )
8 5 6 7 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∈ V )
9 feq1 ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ↔ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ) )
10 coeq1 ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ℎ ∘ ( inl ↾ 𝐴 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) )
11 10 eqeq1d ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ↔ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ) )
12 coeq1 ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ℎ ∘ ( inr ↾ 𝐵 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) )
13 12 eqeq1d ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ↔ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )
14 9 11 13 3anbi123d ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ↔ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) )
15 eqeq1 ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ℎ = 𝑘 ↔ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) )
16 15 imbi2d ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ℎ = 𝑘 ) ↔ ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) ) )
17 16 ralbidv ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) → ( ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ℎ = 𝑘 ) ↔ ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) ) )
18 14 17 anbi12d ⊢ ( ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ 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 ‘ 𝑥 ) ) ) ) = 𝑘 ) ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ ℎ = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ 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 ‘ 𝑥 ) ) ) ) = 𝑘 ) ) ) )
20 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
21 1 2 20 updjudhf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 )
22 1 2 20 updjudhcoinlf ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 )
23 1 2 20 updjudhcoinrg ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 )
24 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ 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 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) ↔ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ) )
26 fvres ⊢ ( 𝑧 ∈ 𝐴 → ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) = ( inl ‘ 𝑧 ) )
27 26 eqcomd ⊢ ( 𝑧 ∈ 𝐴 → ( inl ‘ 𝑧 ) = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) )
28 27 eqeq2d ⊢ ( 𝑧 ∈ 𝐴 → ( 𝑦 = ( inl ‘ 𝑧 ) ↔ 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
29 28 adantl ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( inl ‘ 𝑧 ) ↔ 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
30 fveq1 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) )
31 30 ad2antrr ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) )
32 inlresf ⊢ ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 )
33 ffn ⊢ ( ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 ) → ( inl ↾ 𝐴 ) Fn 𝐴 )
34 32 33 mp1i ⊢ ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) → ( inl ↾ 𝐴 ) Fn 𝐴 )
35 fvco2 ⊢ ( ( ( inl ↾ 𝐴 ) Fn 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
36 34 35 sylan ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
37 fvco2 ⊢ ( ( ( inl ↾ 𝐴 ) Fn 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( 𝑘 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
38 34 37 sylan ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑧 ) = ( 𝑘 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
39 31 36 38 3eqtr3d ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
40 fveq2 ⊢ ( 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
41 fveq2 ⊢ ( 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) → ( 𝑘 ‘ 𝑦 ) = ( 𝑘 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) )
42 40 41 eqeq12d ⊢ ( 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ↔ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) ) ) )
43 39 42 syl5ibrcom ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( ( inl ↾ 𝐴 ) ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
44 29 43 sylbid ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( inl ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
45 44 expimpd ⊢ ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) ∧ 𝜑 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
46 45 ex ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) → ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
47 46 eqcoms ⊢ ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) → ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
48 25 47 syl6bir ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
49 48 com23 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( 𝜑 → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
50 49 3ad2ant2 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝜑 → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
51 50 impcom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
52 51 com12 ⊢ ( ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 → ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
53 52 3ad2ant2 ⊢ ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
54 53 impcom ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
55 54 com12 ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( inl ‘ 𝑧 ) ) → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
56 55 rexlimiva ⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( inl ‘ 𝑧 ) → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
57 eqeq2 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) ↔ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )
58 fvres ⊢ ( 𝑧 ∈ 𝐵 → ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) = ( inr ‘ 𝑧 ) )
59 58 eqcomd ⊢ ( 𝑧 ∈ 𝐵 → ( inr ‘ 𝑧 ) = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) )
60 59 eqeq2d ⊢ ( 𝑧 ∈ 𝐵 → ( 𝑦 = ( inr ‘ 𝑧 ) ↔ 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
61 60 adantl ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 = ( inr ‘ 𝑧 ) ↔ 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
62 fveq1 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) )
63 62 ad2antrr ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) )
64 inrresf ⊢ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )
65 ffn ⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) → ( inr ↾ 𝐵 ) Fn 𝐵 )
66 64 65 mp1i ⊢ ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) → ( inr ↾ 𝐵 ) Fn 𝐵 )
67 fvco2 ⊢ ( ( ( inr ↾ 𝐵 ) Fn 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
68 66 67 sylan ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
69 fvco2 ⊢ ( ( ( inr ↾ 𝐵 ) Fn 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( 𝑘 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
70 66 69 sylan ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑧 ) = ( 𝑘 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
71 63 68 70 3eqtr3d ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) = ( 𝑘 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
72 fveq2 ⊢ ( 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
73 fveq2 ⊢ ( 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) → ( 𝑘 ‘ 𝑦 ) = ( 𝑘 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) )
74 72 73 eqeq12d ⊢ ( 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ↔ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) = ( 𝑘 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) ) ) )
75 71 74 syl5ibrcom ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 = ( ( inr ↾ 𝐵 ) ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
76 61 75 sylbid ⊢ ( ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 = ( inr ‘ 𝑧 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
77 76 expimpd ⊢ ( ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) ∧ 𝜑 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
78 77 ex ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) → ( 𝜑 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
79 78 eqcoms ⊢ ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) → ( 𝜑 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
80 57 79 syl6bir ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( 𝜑 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
81 80 com23 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( 𝜑 → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
82 81 3ad2ant3 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝜑 → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) ) )
83 82 impcom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
84 83 com12 ⊢ ( ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 → ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
85 84 3ad2ant3 ⊢ ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) ) )
86 85 impcom ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
87 86 com12 ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
88 87 rexlimiva ⊢ ( ∃ 𝑧 ∈ 𝐵 𝑦 = ( inr ‘ 𝑧 ) → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
89 56 88 jaoi ⊢ ( ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( inl ‘ 𝑧 ) ∨ ∃ 𝑧 ∈ 𝐵 𝑦 = ( inr ‘ 𝑧 ) ) → ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
90 djur ⊢ ( 𝑦 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( inl ‘ 𝑧 ) ∨ ∃ 𝑧 ∈ 𝐵 𝑦 = ( inr ‘ 𝑧 ) ) )
91 89 90 syl11 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( 𝑦 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
92 91 ralrimiv ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ∀ 𝑦 ∈ ( 𝐴 ⊔ 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) )
93 ffn ⊢ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) Fn ( 𝐴 ⊔ 𝐵 ) )
94 93 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) Fn ( 𝐴 ⊔ 𝐵 ) )
95 94 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) Fn ( 𝐴 ⊔ 𝐵 ) )
96 ffn ⊢ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 → 𝑘 Fn ( 𝐴 ⊔ 𝐵 ) )
97 96 3ad2ant1 ⊢ ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → 𝑘 Fn ( 𝐴 ⊔ 𝐵 ) )
98 eqfnfv ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) Fn ( 𝐴 ⊔ 𝐵 ) ∧ 𝑘 Fn ( 𝐴 ⊔ 𝐵 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ↔ ∀ 𝑦 ∈ ( 𝐴 ⊔ 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
99 95 97 98 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ↔ ∀ 𝑦 ∈ ( 𝐴 ⊔ 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝑘 ‘ 𝑦 ) ) )
100 92 99 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) ∧ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 )
101 100 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) )
102 101 ralrimivw ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) → ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) )
103 24 102 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ 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 ‘ 𝑥 ) ) ) ) = 𝑘 ) ) )
104 103 ex ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ 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 ‘ 𝑥 ) ) ) ) = 𝑘 ) ) ) )
105 21 22 23 104 mp3and ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ∧ ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ) = 𝑘 ) ) )
106 8 19 105 rspcedvd ⊢ ( 𝜑 → ∃ ℎ ∈ V ( ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ∧ ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ℎ = 𝑘 ) ) )
107 feq1 ⊢ ( ℎ = 𝑘 → ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ↔ 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ) )
108 coeq1 ⊢ ( ℎ = 𝑘 → ( ℎ ∘ ( inl ↾ 𝐴 ) ) = ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) )
109 108 eqeq1d ⊢ ( ℎ = 𝑘 → ( ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ↔ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ) )
110 coeq1 ⊢ ( ℎ = 𝑘 → ( ℎ ∘ ( inr ↾ 𝐵 ) ) = ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) )
111 110 eqeq1d ⊢ ( ℎ = 𝑘 → ( ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ↔ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )
112 107 109 111 3anbi123d ⊢ ( ℎ = 𝑘 → ( ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ↔ ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ) )
113 112 reu8 ⊢ ( ∃! ℎ ∈ V ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ↔ ∃ ℎ ∈ V ( ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ∧ ∀ 𝑘 ∈ V ( ( 𝑘 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( 𝑘 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( 𝑘 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) → ℎ = 𝑘 ) ) )
114 106 113 sylibr ⊢ ( 𝜑 → ∃! ℎ ∈ V ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )
115 reuv ⊢ ( ∃! ℎ ∈ V ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) ↔ ∃! ℎ ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )
116 114 115 sylib ⊢ ( 𝜑 → ∃! ℎ ( ℎ : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 ∧ ( ℎ ∘ ( inl ↾ 𝐴 ) ) = 𝐹 ∧ ( ℎ ∘ ( inr ↾ 𝐵 ) ) = 𝐺 ) )