Metamath Proof Explorer

Theorem frinxp

Description: Intersection of well-founded relation with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)

Ref Expression
Assertion frinxp 
|- ( R Fr A <-> ( R i^i ( A X. A ) ) Fr A )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( z C_ A -> ( x e. z -> x e. A ) )
2 ssel 
 |-  ( z C_ A -> ( y e. z -> y e. A ) )
3 1 2 anim12d 
 |-  ( z C_ A -> ( ( x e. z /\ y e. z ) -> ( x e. A /\ y e. A ) ) )
4 brinxp 
 |-  ( ( y e. A /\ x e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
5 4 ancoms 
 |-  ( ( x e. A /\ y e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
6 3 5 syl6 
 |-  ( z C_ A -> ( ( x e. z /\ y e. z ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) ) )
7 6 impl 
 |-  ( ( ( z C_ A /\ x e. z ) /\ y e. z ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
8 7 notbid 
 |-  ( ( ( z C_ A /\ x e. z ) /\ y e. z ) -> ( -. y R x <-> -. y ( R i^i ( A X. A ) ) x ) )
9 8 ralbidva 
 |-  ( ( z C_ A /\ x e. z ) -> ( A. y e. z -. y R x <-> A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
10 9 rexbidva 
 |-  ( z C_ A -> ( E. x e. z A. y e. z -. y R x <-> E. x e. z A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
11 10 adantr 
 |-  ( ( z C_ A /\ z =/= (/) ) -> ( E. x e. z A. y e. z -. y R x <-> E. x e. z A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
12 11 pm5.74i 
 |-  ( ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) <-> ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
13 12 albii 
 |-  ( A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
14 df-fr 
 |-  ( R Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) )
15 df-fr 
 |-  ( ( R i^i ( A X. A ) ) Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y ( R i^i ( A X. A ) ) x ) )
16 13 14 15 3bitr4i 
 |-  ( R Fr A <-> ( R i^i ( A X. A ) ) Fr A )