Theorem isfth

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

	Ref	Expression
Hypothesis	isfth.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	isfth	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfth.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		fthfunc	⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
3	2	ssbri	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
4		df-br	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
5		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
6	4 5	sylbi	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
7		oveq12	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
8	7	breqd	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ↔ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) )
9		simpl	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
10	9	fveq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
11	10 1	eqtr4di	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = 𝐵 )
12	11	raleqdv	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) )
13	11 12	raleqbidv	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) )
14	8 13	anbi12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) ↔ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) ) )
15	14	opabbidv	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
16		df-fth	⊢ Faith = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
17		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
18		simpl	⊢ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
19	18	ssopab2i	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ⊆ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 }
20		opabss	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 } ⊆ ( 𝐶 Func 𝐷 )
21	19 20	sstri	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ⊆ ( 𝐶 Func 𝐷 )
22	17 21	ssexi	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } ∈ V
23	15 16 22	ovmpoa	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Faith 𝐷 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
24	6 23	syl	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 Faith 𝐷 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
25	24	breqd	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } 𝐺 ) )
26		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
27	26	brrelex12i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
28		breq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) )
29		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
30	29	oveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
31	30	cnveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ◡ ( 𝑥 𝑔 𝑦 ) = ◡ ( 𝑥 𝐺 𝑦 ) )
32	31	funeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( Fun ◡ ( 𝑥 𝑔 𝑦 ) ↔ Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
33	32	2ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
34	28 33	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ) )
35		eqid	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) }
36	34 35	brabga	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ) )
37	27 36	syl	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ) )
38	25 37	bitrd	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) ) )
39	38	bianabs	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )
40	3 39	biadanii	⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 Fun ◡ ( 𝑥 𝐺 𝑦 ) ) )