Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

	Ref	Expression
Assertion	idref	⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
2	1	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ↔ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 )
3		opex	⊢ ⟨ 𝑥 , 𝑥 ⟩ ∈ V
4	3 1	fnmpti	⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) Fn 𝐴
5		df-f	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 ) )
6	4 5	mpbiran	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
7	2 6	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
8		df-br	⊢ ( 𝑥 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
10		mptresid	⊢ ( I ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
11		vex	⊢ 𝑥 ∈ V
12	11	fnasrn	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
13	10 12	eqtri	⊢ ( I ↾ 𝐴 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
14	13	sseq1i	⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
15	7 9 14	3bitr4ri	⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )