This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem initoeu2lem2

Description: Lemma 2 for initoeu2 . (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
initoeu2lem.x ⊢ 𝑋 = ( Base ‘ 𝐶 )
initoeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
initoeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
initoeu2lem.o ⊢ ⚬ = ( comp ‘ 𝐶 )
Assertion initoeu2lem2 ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu2lem.x ⊢ 𝑋 = ( Base ‘ 𝐶 )
4 initoeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 initoeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
6 initoeu2lem.o ⊢ ⚬ = ( comp ‘ 𝐶 )
7 ovex ⊢ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ V
8 eleq1 ⊢ ( 𝑔 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) → ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ↔ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
9 8 spcegv ⊢ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ V → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )
10 7 9 mp1i ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )
11 10 com12 ⊢ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝜑 → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝜑 → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )
13 12 com12 ⊢ ( 𝜑 → ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )
14 13 a1d ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) ) )
15 14 3imp ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) )
17 simpll1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝜑 )
18 simpll2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
19 3simpb ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
20 19 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
22 21 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) )
24 simpl32 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) )
25 24 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) )
26 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) )
27 1 2 3 4 5 6 initoeu2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
28 27 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝑔 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
29 17 18 22 23 25 26 28 syl33anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
30 29 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝑔 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
31 simpll1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝜑 )
32 simpll2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
33 21 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) )
34 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) )
35 24 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) )
36 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ℎ ∈ ( 𝐵 𝐻 𝐷 ) )
37 1 2 3 4 5 6 initoeu2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ℎ = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
38 37 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ℎ = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
39 31 32 33 34 35 36 38 syl33anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → ℎ = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
40 39 adantrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ℎ = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
41 30 40 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝑔 = ℎ )
42 41 ex ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → ( ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 = ℎ ) )
43 42 alrimivv ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → ∀ 𝑔 ∀ ℎ ( ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 = ℎ ) )
44 eleq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ↔ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) )
45 44 eu4 ⊢ ( ∃! 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ↔ ( ∃ 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ∀ 𝑔 ∀ ℎ ( ( 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ∧ ℎ ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝑔 = ℎ ) ) )
46 16 43 45 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) ∧ ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) )
47 46 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) → ∃! 𝑔 𝑔 ∈ ( 𝐵 𝐻 𝐷 ) ) )