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

Metamath Proof Explorer

Theorem fullthinc2

Description: A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses fullthinc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fullthinc.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
fullthinc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fullthinc.d ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
fullthinc2.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
fullthinc2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fullthinc2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion fullthinc2 ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 fullthinc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fullthinc.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
3 fullthinc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 fullthinc.d ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
5 fullthinc2.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
6 fullthinc2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 fullthinc2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 fullfunc ⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
9 8 ssbri ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
10 5 9 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
11 1 2 3 4 10 fullthinc ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
12 5 11 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
13 oveq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
14 13 eqeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑋 𝐻 𝑌 ) = ∅ ) )
15 simpl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
16 15 fveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
17 simpr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
18 17 fveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
19 16 18 oveq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
20 19 eqeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ↔ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )
21 14 20 imbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ↔ ( ( 𝑋 𝐻 𝑌 ) = ∅ → ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) ) )
22 21 rspc2gv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑋 𝐻 𝑌 ) = ∅ → ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) ) )
23 22 imp ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → ( ( 𝑋 𝐻 𝑌 ) = ∅ → ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )
24 6 7 12 23 syl21anc ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) = ∅ → ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )
25 1 3 2 10 6 7 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
26 25 f002 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )
27 24 26 impbid ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )