Metamath Proof Explorer


Theorem relintab

Description: Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020)

Ref Expression
Assertion relintab Rel x | φ x | φ = w 𝒫 V × V | x w = x -1 -1 φ

Proof

Step Hyp Ref Expression
1 cnvcnv x | φ -1 -1 = x | φ V × V
2 incom x | φ V × V = V × V x | φ
3 1 2 eqtri x | φ -1 -1 = V × V x | φ
4 dfrel2 Rel x | φ x | φ -1 -1 = x | φ
5 4 biimpi Rel x | φ x | φ -1 -1 = x | φ
6 relintabex Rel x | φ x φ
7 6 xpinintabd Rel x | φ V × V x | φ = w 𝒫 V × V | x w = V × V x φ
8 incom V × V x = x V × V
9 cnvcnv x -1 -1 = x V × V
10 8 9 eqtr4i V × V x = x -1 -1
11 10 eqeq2i w = V × V x w = x -1 -1
12 11 anbi1i w = V × V x φ w = x -1 -1 φ
13 12 exbii x w = V × V x φ x w = x -1 -1 φ
14 13 rabbii w 𝒫 V × V | x w = V × V x φ = w 𝒫 V × V | x w = x -1 -1 φ
15 14 inteqi w 𝒫 V × V | x w = V × V x φ = w 𝒫 V × V | x w = x -1 -1 φ
16 7 15 syl6eq Rel x | φ V × V x | φ = w 𝒫 V × V | x w = x -1 -1 φ
17 3 5 16 3eqtr3a Rel x | φ x | φ = w 𝒫 V × V | x w = x -1 -1 φ