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

Metamath Proof Explorer

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 vsnex ⊢ { 𝑥 } ∈ V
3 2 cnvex ⊢ ◡ { 𝑥 } ∈ V
4 3 uniex ⊢ ∪ ◡ { 𝑥 } ∈ V
5 4 a1i ⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∪ ◡ { 𝑥 } ∈ V )
6 vsnex ⊢ { 𝑦 } ∈ 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→ ◡ 𝐴 )