Theorem isfth 17639

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

Hypothesis

Ref	Expression
isfth.b	⊢ 𝐵 = (Base‘𝐶)

Assertion

Ref	Expression
isfth	⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦

Proof of Theorem isfth

Dummy variables 𝑐 𝑑 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fthfunc 17632	. . 3 ⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
2	1	ssbri 5120	. 2 ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 → 𝐹(𝐶 Func 𝐷)𝐺)
3		df-br 5076	. . . . . . 7 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
4		funcrcl 17587	. . . . . . 7 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
5	3, 4	sylbi 216	. . . . . 6 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
6		oveq12 7293	. . . . . . . . . 10 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷))
7	6	breqd 5086	. . . . . . . . 9 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝑓(𝑐 Func 𝑑)𝑔 ↔ 𝑓(𝐶 Func 𝐷)𝑔))
8		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑐 = 𝐶)
9	8	fveq2d 6787	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶))
10		isfth.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐶)
11	9, 10	eqtr4di 2797	. . . . . . . . . 10 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = 𝐵)
12	11	raleqdv 3349	. . . . . . . . . 10 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)))
13	11, 12	raleqbidv 3337	. . . . . . . . 9 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)))
14	7, 13	anbi12d 631	. . . . . . . 8 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦)) ↔ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))))
15	14	opabbidv 5141	. . . . . . 7 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))})
16		df-fth 17630	. . . . . . 7 ⊢ Faith = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))})
17		ovex 7317	. . . . . . . 8 ⊢ (𝐶 Func 𝐷) ∈ V
18		simpl 483	. . . . . . . . . 10 ⊢ ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)) → 𝑓(𝐶 Func 𝐷)𝑔)
19	18	ssopab2i 5464	. . . . . . . . 9 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔}
20		opabss 5139	. . . . . . . . 9 ⊢ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔} ⊆ (𝐶 Func 𝐷)
21	19, 20	sstri 3931	. . . . . . . 8 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ⊆ (𝐶 Func 𝐷)
22	17, 21	ssexi 5247	. . . . . . 7 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ∈ V
23	15, 16, 22	ovmpoa 7437	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Faith 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))})
24	5, 23	syl 17	. . . . 5 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 Faith 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))})
25	24	breqd 5086	. . . 4 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺))
26		relfunc 17586	. . . . . 6 ⊢ Rel (𝐶 Func 𝐷)
27	26	brrelex12i 5643	. . . . 5 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
28		breq12 5080	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(𝐶 Func 𝐷)𝑔 ↔ 𝐹(𝐶 Func 𝐷)𝐺))
29		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
30	29	oveqd 7301	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
31	30	cnveqd 5787	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ◡(𝑥𝑔𝑦) = ◡(𝑥𝐺𝑦))
32	31	funeqd 6463	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (Fun ◡(𝑥𝑔𝑦) ↔ Fun ◡(𝑥𝐺𝑦)))
33	32	2ralbidv 3130	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))
34	28, 33	anbi12d 631	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)) ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))))
35		eqid 2739	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}
36	34, 35	brabga 5448	. . . . 5 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))))
37	27, 36	syl 17	. . . 4 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))))
38	25, 37	bitrd 278	. . 3 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))))
39	38	bianabs 542	. 2 ⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))
40	2, 39	biadanii 819	1 ⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065  Vcvv 3433  ⟨cop 4568   class class class wbr 5075  {copab 5137  ^◡ccnv 5589  Fun wfun 6431  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  Catccat 17382   Func cfunc 17578   Faith cfth 17628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-func 17582  df-fth 17630

This theorem is referenced by:  isfth2  17640  fthpropd  17646  fthoppc  17648  fthres2b  17655  fthres2c  17656  fthres2  17657