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

Metamath Proof Explorer

Theorem updjud

Proof