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

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 ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
setciso.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion setciso ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 setcmon.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcmon.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 setcmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
4 setcmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5 setciso.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
8 1 setccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
9 2 8 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 1 2 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
11 3 10 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
12 4 10 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
13 6 7 9 11 12 5 isoval ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
15 6 7 9 11 12 invfun ⊢ ( 𝜑 → Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
16 funfvbrb ⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
17 15 16 syl ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
18 1 2 3 4 7 setcinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ◡ 𝐹 ) ) )
19 simpl ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) = ◡ 𝐹 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
20 18 19 biimtrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
21 17 20 sylbid ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
22 eqid ⊢ ◡ 𝐹 = ◡ 𝐹
23 1 2 3 4 7 setcinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ◡ 𝐹 = ◡ 𝐹 ) ) )
24 funrel ⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
25 15 24 syl ⊢ ( 𝜑 → Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
26 releldm ⊢ ( ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ∧ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
27 26 ex ⊢ ( Rel ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
28 25 27 syl ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ◡ 𝐹 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
29 23 28 sylbird ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ◡ 𝐹 = ◡ 𝐹 ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
30 22 29 mpan2i ⊢ ( 𝜑 → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
31 21 30 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
32 14 31 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )