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

Metamath Proof Explorer

Theorem dfcnv2

Description: Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018)

Ref Expression
Assertion dfcnv2 ( ran 𝑅 ⊆ 𝐴 → ◡ 𝑅 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ◡ 𝑅
2 relxp ⊢ Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) )
3 2 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) )
4 reliun ⊢ ( Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) )
5 3 4 mpbir ⊢ Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) )
6 vex ⊢ 𝑧 ∈ V
7 vex ⊢ 𝑦 ∈ V
8 6 7 opeldm ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 → 𝑧 ∈ dom ◡ 𝑅 )
9 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
10 8 9 eleqtrrdi ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 → 𝑧 ∈ ran 𝑅 )
11 ssel2 ⊢ ( ( ran 𝑅 ⊆ 𝐴 ∧ 𝑧 ∈ ran 𝑅 ) → 𝑧 ∈ 𝐴 )
12 10 11 sylan2 ⊢ ( ( ran 𝑅 ⊆ 𝐴 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ) → 𝑧 ∈ 𝐴 )
13 12 ex ⊢ ( ran 𝑅 ⊆ 𝐴 → ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 → 𝑧 ∈ 𝐴 ) )
14 13 pm4.71rd ⊢ ( ran 𝑅 ⊆ 𝐴 → ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ↔ ( 𝑧 ∈ 𝐴 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ) ) )
15 6 7 elimasn ⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 )
16 15 anbi2i ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ) )
17 14 16 bitr4di ⊢ ( ran 𝑅 ⊆ 𝐴 → ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) ) )
18 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
19 18 imaeq2d ⊢ ( 𝑥 = 𝑧 → ( ◡ 𝑅 “ { 𝑥 } ) = ( ◡ 𝑅 “ { 𝑧 } ) )
20 19 opeliunxp2 ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) )
21 17 20 bitr4di ⊢ ( ran 𝑅 ⊆ 𝐴 → ( ⟨ 𝑧 , 𝑦 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ) )
22 1 5 21 eqrelrdv ⊢ ( ran 𝑅 ⊆ 𝐴 → ◡ 𝑅 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) )