Description: A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | cnven | ⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ≈ ◡ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | ⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 ) | |
2 | cnvexg | ⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V ) | |
3 | 2 | adantl | ⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ◡ 𝐴 ∈ V ) |
4 | cnvf1o | ⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 ) | |
5 | 4 | adantr | ⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 ) |
6 | f1oen2g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ◡ 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 ) → 𝐴 ≈ ◡ 𝐴 ) | |
7 | 1 3 5 6 | syl3anc | ⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ≈ ◡ 𝐴 ) |