Metamath Proof Explorer

Theorem fthfunc

Description: A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion fthfunc ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 Faith 𝑑 ) = ( 𝐶 Faith 𝑑 ) )
2 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝑑 ) )
3 1 2 sseq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 Faith 𝑑 ) ⊆ ( 𝑐 Func 𝑑 ) ↔ ( 𝐶 Faith 𝑑 ) ⊆ ( 𝐶 Func 𝑑 ) ) )
4 oveq2 ⊢ ( 𝑑 = 𝐷 → ( 𝐶 Faith 𝑑 ) = ( 𝐶 Faith 𝐷 ) )
5 oveq2 ⊢ ( 𝑑 = 𝐷 → ( 𝐶 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
6 4 5 sseq12d ⊢ ( 𝑑 = 𝐷 → ( ( 𝐶 Faith 𝑑 ) ⊆ ( 𝐶 Func 𝑑 ) ↔ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) ) )
7 ovex ⊢ ( 𝑐 Func 𝑑 ) ∈ V
8 simpl ⊢ ( ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) → 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 )
9 8 ssopab2i ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ⊆ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 }
10 opabss ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 } ⊆ ( 𝑐 Func 𝑑 )
11 9 10 sstri ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ⊆ ( 𝑐 Func 𝑑 )
12 7 11 ssexi ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ∈ V
13 df-fth ⊢ Faith = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
14 13 ovmpt4g ⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ∧ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ∈ V ) → ( 𝑐 Faith 𝑑 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
15 12 14 mp3an3 ⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ) → ( 𝑐 Faith 𝑑 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
16 15 11 eqsstrdi ⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ) → ( 𝑐 Faith 𝑑 ) ⊆ ( 𝑐 Func 𝑑 ) )
17 3 6 16 vtocl2ga ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) )
18 13 mpondm0 ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Faith 𝐷 ) = ∅ )
19 0ss ⊢ ∅ ⊆ ( 𝐶 Func 𝐷 )
20 18 19 eqsstrdi ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) )
21 17 20 pm2.61i ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )