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 𝑅 ⊆ 𝐴 → ◡ 𝑅 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) )