Metamath Proof Explorer

Theorem setciso

Description: An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c ⊢ C = SetCat ⁡ U
setcmon.u ⊢ φ → U ∈ V
setcmon.x ⊢ φ → X ∈ U
setcmon.y ⊢ φ → Y ∈ U
setciso.n ⊢ I = Iso ⁡ C
Assertion setciso ⊢ φ → F ∈ X I Y ↔ F : X ⟶ 1-1 onto Y

Proof

Step Hyp Ref Expression
1 setcmon.c ⊢ C = SetCat ⁡ U
2 setcmon.u ⊢ φ → U ∈ V
3 setcmon.x ⊢ φ → X ∈ U
4 setcmon.y ⊢ φ → Y ∈ U
5 setciso.n ⊢ I = Iso ⁡ C
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Inv ⁡ C = Inv ⁡ C
8 1 setccat ⊢ U ∈ V → C ∈ Cat
9 2 8 syl ⊢ φ → C ∈ Cat
10 1 2 setcbas ⊢ φ → U = Base C
11 3 10 eleqtrd ⊢ φ → X ∈ Base C
12 4 10 eleqtrd ⊢ φ → Y ∈ Base C
13 6 7 9 11 12 5 isoval ⊢ φ → X I Y = dom ⁡ X Inv ⁡ C Y
14 13 eleq2d ⊢ φ → F ∈ X I Y ↔ F ∈ dom ⁡ X Inv ⁡ C Y
15 6 7 9 11 12 invfun ⊢ φ → Fun ⁡ X Inv ⁡ C Y
16 funfvbrb ⊢ Fun ⁡ X Inv ⁡ C Y → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F
17 15 16 syl ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F
18 1 2 3 4 7 setcinv ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F ↔ F : X ⟶ 1-1 onto Y ∧ X Inv ⁡ C Y ⁡ F = F -1
19 simpl ⊢ F : X ⟶ 1-1 onto Y ∧ X Inv ⁡ C Y ⁡ F = F -1 → F : X ⟶ 1-1 onto Y
20 18 19 syl6bi ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F → F : X ⟶ 1-1 onto Y
21 17 20 sylbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y → F : X ⟶ 1-1 onto Y
22 eqid ⊢ F -1 = F -1
23 1 2 3 4 7 setcinv ⊢ φ → F X Inv ⁡ C Y F -1 ↔ F : X ⟶ 1-1 onto Y ∧ F -1 = F -1
24 funrel ⊢ Fun ⁡ X Inv ⁡ C Y → Rel ⁡ X Inv ⁡ C Y
25 15 24 syl ⊢ φ → Rel ⁡ X Inv ⁡ C Y
26 releldm ⊢ Rel ⁡ X Inv ⁡ C Y ∧ F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
27 26 ex ⊢ Rel ⁡ X Inv ⁡ C Y → F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
28 25 27 syl ⊢ φ → F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
29 23 28 sylbird ⊢ φ → F : X ⟶ 1-1 onto Y ∧ F -1 = F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
30 22 29 mpan2i ⊢ φ → F : X ⟶ 1-1 onto Y → F ∈ dom ⁡ X Inv ⁡ C Y
31 21 30 impbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F : X ⟶ 1-1 onto Y
32 14 31 bitrd ⊢ φ → F ∈ X I Y ↔ F : X ⟶ 1-1 onto Y