Metamath Proof Explorer

Theorem fullthinc

Description: A functor to a thin category is full iff empty hom-sets are mapped 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 )
fullthinc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion fullthinc ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 fullthinc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fullthinc.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
3 fullthinc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 fullthinc.d ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
5 fullthinc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
6 1 2 3 isfull2 ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
7 foeq2 ⊢ ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ∅ –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
8 fo00 ⊢ ( ( 𝑥 𝐺 𝑦 ) : ∅ –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
9 8 simprbi ⊢ ( ( 𝑥 𝐺 𝑦 ) : ∅ –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ )
10 7 9 syl6bi ⊢ ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
11 10 com12 ⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
12 11 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
13 6 12 simplbiim ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
14 13 adantl ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
15 simplr ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
16 imor ⊢ ( ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ↔ ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ∨ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
17 simplr ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
18 simprl ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
19 simprr ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
20 1 3 2 17 18 19 funcf2 ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
21 20 adantr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
22 simpr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ¬ ( 𝑥 𝐻 𝑦 ) = ∅ )
23 22 neqned ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑥 𝐻 𝑦 ) ≠ ∅ )
24 fdomne0 ⊢ ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) → ( ( 𝑥 𝐺 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ) )
25 21 23 24 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( ( 𝑥 𝐺 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ) )
26 25 simprd ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
27 simplll ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝐷 ∈ ThinCat )
28 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
29 17 adantr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
30 1 28 29 funcf1 ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
31 18 adantr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝑥 ∈ 𝐵 )
32 30 31 ffvelrnd ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
33 19 adantr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝑦 ∈ 𝐵 )
34 30 33 ffvelrnd ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
35 eqidd ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
36 2 a1i ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → 𝐽 = ( Hom ‘ 𝐷 ) )
37 27 32 34 35 36 thincn0eu ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ↔ ∃! 𝑓 𝑓 ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
38 26 37 mpbid ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ∃! 𝑓 𝑓 ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
39 eusn ⊢ ( ∃! 𝑓 𝑓 ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑓 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } )
40 38 39 sylib ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ∃ 𝑓 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } )
41 25 simpld ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) ≠ ∅ )
42 foconst ⊢ ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ { 𝑓 } ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ { 𝑓 } )
43 feq3 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ { 𝑓 } ) )
44 43 anbi1d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) ↔ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ { 𝑓 } ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) ) )
45 foeq3 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ { 𝑓 } ) )
46 44 45 imbi12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ { 𝑓 } ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ { 𝑓 } ) ) )
47 42 46 mpbiri ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
48 47 exlimiv ⊢ ( ∃ 𝑓 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } → ( ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
49 48 imp ⊢ ( ( ∃ 𝑓 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = { 𝑓 } ∧ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑥 𝐺 𝑦 ) ≠ ∅ ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
50 40 21 41 49 syl12anc ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
51 20 adantr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
52 feq3 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ∅ ) )
53 52 adantl ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ∅ ) )
54 51 53 mpbid ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ∅ )
55 f00 ⊢ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ∅ ↔ ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( 𝑥 𝐻 𝑦 ) = ∅ ) )
56 54 55 sylib ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( 𝑥 𝐻 𝑦 ) = ∅ ) )
57 56 simprd ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐻 𝑦 ) = ∅ )
58 56 simpld ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) = ∅ )
59 simpr ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ )
60 8 biimpri ⊢ ( ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ∅ –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
61 60 7 syl5ibr ⊢ ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
62 61 imp ⊢ ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ∧ ( ( 𝑥 𝐺 𝑦 ) = ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
63 57 58 59 62 syl12anc ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
64 50 63 jaodan ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ∨ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
65 16 64 sylan2b ⊢ ( ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
66 65 ex ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
67 66 ralimdvva ⊢ ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
68 67 imp ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) –onto→ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
69 15 68 6 sylanbrc ⊢ ( ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
70 14 69 impbida ⊢ ( ( 𝐷 ∈ ThinCat ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
71 4 5 70 syl2anc ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )