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	syl6bi	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( 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→ 𝑌 ) )

Metamath Proof Explorer

Theorem setciso

Proof