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

Metamath Proof Explorer

Theorem fullfo

Description: The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfull.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isfull.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
isfull.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fullfo.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
fullfo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fullfo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion fullfo ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 isfull.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isfull.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
3 isfull.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 fullfo.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
5 fullfo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 fullfo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 1 2 3 isfull2 ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
8 7 simprbi ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
9 4 8 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
10 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
13 11 12 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
14 11 12 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
15 11 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
16 12 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
17 15 16 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
18 13 14 17 foeq123d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
19 10 18 rspcdv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
20 5 19 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
21 9 20 mpd ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )