Theorem isofn 17857

Description: The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020.)

Assertion

Ref	Expression
isofn	⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))

Proof of Theorem isofn

Dummy variables 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmexg 7907	. . . . . 6 ⊢ (𝑥 ∈ V → dom 𝑥 ∈ V)
2	1	adantl 487	. . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝑥 ∈ V) → dom 𝑥 ∈ V)
3	2	ralrimiva 3160	. . . 4 ⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ V dom 𝑥 ∈ V)
4		eqid 2766	. . . . 5 ⊢ (𝑥 ∈ V ↦ dom 𝑥) = (𝑥 ∈ V ↦ dom 𝑥)
5	4	fnmpt 6682	. . . 4 ⊢ (∀𝑥 ∈ V dom 𝑥 ∈ V → (𝑥 ∈ V ↦ dom 𝑥) Fn V)
6	3, 5	syl 18	. . 3 ⊢ (𝐶 ∈ Cat → (𝑥 ∈ V ↦ dom 𝑥) Fn V)
7		ovex 7456	. . . . . . . 8 ⊢ (𝑥(Sect‘𝐶)𝑦) ∈ V
8	7	inex1 5291	. . . . . . 7 ⊢ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V
9	8	a1i 11	. . . . . 6 ⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V)
10	9	ralrimivva 3211	. . . . 5 ⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V)
11		eqid 2766	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))
12	11	fnmpo 8075	. . . . 5 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶)))
13	10, 12	syl 18	. . . 4 ⊢ (𝐶 ∈ Cat → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶)))
14		df-inv 17830	. . . . . 6 ⊢ Inv = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))))
15		fveq2 6888	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶))
16		fveq2 6888	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (Sect‘𝑐) = (Sect‘𝐶))
17	16	oveqd 7440	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑥(Sect‘𝑐)𝑦) = (𝑥(Sect‘𝐶)𝑦))
18	16	oveqd 7440	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑦(Sect‘𝑐)𝑥) = (𝑦(Sect‘𝐶)𝑥))
19	18	cnveqd 5866	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ◡(𝑦(Sect‘𝑐)𝑥) = ◡(𝑦(Sect‘𝐶)𝑥))
20	17, 19	ineq12d 4177	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥)) = ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))
21	15, 15, 20	mpoeq123dv 7498	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ ((𝑥(Sect‘𝑐)𝑦) ∩ ◡(𝑦(Sect‘𝑐)𝑥))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))))
22		id 23	. . . . . 6 ⊢ (𝐶 ∈ Cat → 𝐶 ∈ Cat)
23		fvex 6901	. . . . . . . 8 ⊢ (Base‘𝐶) ∈ V
24	23, 23	pm3.2i 476	. . . . . . 7 ⊢ ((Base‘𝐶) ∈ V ∧ (Base‘𝐶) ∈ V)
25		mpoexga 8083	. . . . . . 7 ⊢ (((Base‘𝐶) ∈ V ∧ (Base‘𝐶) ∈ V) → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) ∈ V)
26	24, 25	mp1i 14	. . . . . 6 ⊢ (𝐶 ∈ Cat → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) ∈ V)
27	14, 21, 22, 26	fvmptd3 7020	. . . . 5 ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))))
28	27	fneq1d 6635	. . . 4 ⊢ (𝐶 ∈ Cat → ((Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn ((Base‘𝐶) × (Base‘𝐶))))
29	13, 28	mpbird 260	. . 3 ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
30		ssv 3964	. . . 4 ⊢ ran (Inv‘𝐶) ⊆ V
31	30	a1i 11	. . 3 ⊢ (𝐶 ∈ Cat → ran (Inv‘𝐶) ⊆ V)
32		fnco 6660	. . 3 ⊢ (((𝑥 ∈ V ↦ dom 𝑥) Fn V ∧ (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ran (Inv‘𝐶) ⊆ V) → ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶)))
33	6, 29, 31, 32	syl3anc 1398	. 2 ⊢ (𝐶 ∈ Cat → ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶)))
34		isofval 17839	. . 3 ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)))
35	34	fneq1d 6635	. 2 ⊢ (𝐶 ∈ Cat → ((Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝐶)) Fn ((Base‘𝐶) × (Base‘𝐶))))
36	33, 35	mpbird 260	1 ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3082  Vcvv 3458   ∩ cin 3907   ⊆ wss 3908   ↦ cmpt 5197   × cxp 5664  ^◡ccnv 5665  dom cdm 5666  ran crn 5667   ∘ ccom 5670   Fn wfn 6538  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425  Basecbs 17294  Catccat 17745  Sectcsect 17826  Invcinv 17827  Isociso 17828

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-inv 17830  df-iso 17831

This theorem is used by:  brcic  17880  ciclcl  17884  cicrcl  17885  cicer  17888  isofval2  49851  isopropdlem  49859  relcic  49864  upeu4  50015