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 𝑅𝐴 𝑅 = 𝑥𝐴 ( { 𝑥 } × ( 𝑅 “ { 𝑥 } ) ) )