Theorem cnvf1o

Description: Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Assertion	cnvf1o	⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } )
2		snex	⊢ { 𝑥 } ∈ V
3	2	cnvex	⊢ ◡ { 𝑥 } ∈ V
4	3	uniex	⊢ ∪ ◡ { 𝑥 } ∈ V
5	4	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∪ ◡ { 𝑥 } ∈ V )
6		snex	⊢ { 𝑦 } ∈ V
7	6	cnvex	⊢ ◡ { 𝑦 } ∈ V
8	7	uniex	⊢ ∪ ◡ { 𝑦 } ∈ V
9	8	a1i	⊢ ( ( Rel 𝐴 ∧ 𝑦 ∈ ◡ 𝐴 ) → ∪ ◡ { 𝑦 } ∈ V )
10		cnvf1olem	⊢ ( ( Rel 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ) → ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) )
11		relcnv	⊢ Rel ◡ 𝐴
12		simpr	⊢ ( ( Rel 𝐴 ∧ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) → ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) )
13		cnvf1olem	⊢ ( ( Rel ◡ 𝐴 ∧ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) → ( 𝑥 ∈ ◡ ◡ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) )
14	11 12 13	sylancr	⊢ ( ( Rel 𝐴 ∧ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) → ( 𝑥 ∈ ◡ ◡ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) )
15		dfrel2	⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
16		eleq2	⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( 𝑥 ∈ ◡ ◡ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
17	15 16	sylbi	⊢ ( Rel 𝐴 → ( 𝑥 ∈ ◡ ◡ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
18	17	anbi1d	⊢ ( Rel 𝐴 → ( ( 𝑥 ∈ ◡ ◡ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ) )
19	18	adantr	⊢ ( ( Rel 𝐴 ∧ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) → ( ( 𝑥 ∈ ◡ ◡ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ) )
20	14 19	mpbid	⊢ ( ( Rel 𝐴 ∧ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) )
21	10 20	impbida	⊢ ( Rel 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ∪ ◡ { 𝑥 } ) ↔ ( 𝑦 ∈ ◡ 𝐴 ∧ 𝑥 = ∪ ◡ { 𝑦 } ) ) )
22	1 5 9 21	f1od	⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 )