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

Metamath Proof Explorer

Theorem isfull

Description: Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfull.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isfull.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
Assertion isfull ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isfull.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isfull.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
3 fullfunc ⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
4 3 ssbri ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
5 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
6 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
7 5 6 sylbi ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
8 oveq12 ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
9 8 breqd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ↔ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) )
10 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
11 10 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
12 11 1 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = 𝐵 )
13 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
14 13 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝐷 ) )
15 14 2 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = 𝐽 )
16 15 oveqd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) )
17 16 eqeq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) )
18 12 17 raleqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) )
19 12 18 raleqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) )
20 9 19 anbi12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) ) )
21 20 opabbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } )
22 df-full ⊢ Full = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
23 ovex ⊢ ( 𝐶 Func 𝐷 ) ∈ V
24 simpl ⊢ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
25 24 ssopab2i ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 }
26 opabss ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 } ⊆ ( 𝐶 Func 𝐷 )
27 25 26 sstri ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ ( 𝐶 Func 𝐷 )
28 23 27 ssexi ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
29 21 22 28 ovmpoa ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Full 𝐷 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } )
30 7 29 syl ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 Full 𝐷 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } )
31 30 breqd ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } 𝐺 ) )
32 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
33 32 brrelex12i ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
34 breq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) )
35 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
36 35 oveqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
37 36 rneqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ran ( 𝑥 𝑔 𝑦 ) = ran ( 𝑥 𝐺 𝑦 ) )
38 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
39 38 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
40 38 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
41 39 40 oveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
42 37 41 eqeq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ↔ ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
43 42 2ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
44 34 43 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
45 eqid ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) }
46 44 45 brabga ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
47 33 46 syl ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ) } 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
48 31 47 bitrd ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) )
49 48 bianabs ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
50 4 49 biadanii ⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )