Metamath Proof Explorer
Description: The identity relation is a function. Part of Theorem 10.4 of Quine
p. 65. See also idfn . (Contributed by NM, 30Apr1998)


Ref 
Expression 

Assertion 
funi 
⊢ Fun I 
Proof
Step 
Hyp 
Ref 
Expression 
1 

reli 
⊢ Rel I 
2 

relcnv 
⊢ Rel ^{◡} I 
3 

coi2 
⊢ ( Rel ^{◡} I → ( I ∘ ^{◡} I ) = ^{◡} I ) 
4 
2 3

axmp 
⊢ ( I ∘ ^{◡} I ) = ^{◡} I 
5 

cnvi 
⊢ ^{◡} I = I 
6 
4 5

eqtri 
⊢ ( I ∘ ^{◡} I ) = I 
7 
6

eqimssi 
⊢ ( I ∘ ^{◡} I ) ⊆ I 
8 

dffun 
⊢ ( Fun I ↔ ( Rel I ∧ ( I ∘ ^{◡} I ) ⊆ I ) ) 
9 
1 7 8

mpbir2an 
⊢ Fun I 