Metamath Proof Explorer

Theorem bnj1154

Description: Property of Fr . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1154 
|- ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. x e. B A. y e. B -. y R x )

Proof

Step Hyp Ref Expression
1 bnj658 
 |-  ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> ( R Fr A /\ B C_ A /\ B =/= (/) ) )
2 elisset 
 |-  ( B e. _V -> E. b b = B )
3 2 bnj708 
 |-  ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. b b = B )
4 df-fr 
 |-  ( R Fr A <-> A. b ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
5 4 biimpi 
 |-  ( R Fr A -> A. b ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
6 5 19.21bi 
 |-  ( R Fr A -> ( ( b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) )
7 6 3impib 
 |-  ( ( R Fr A /\ b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x )
8 sseq1 
 |-  ( b = B -> ( b C_ A <-> B C_ A ) )
9 neeq1 
 |-  ( b = B -> ( b =/= (/) <-> B =/= (/) ) )
10 8 9 3anbi23d 
 |-  ( b = B -> ( ( R Fr A /\ b C_ A /\ b =/= (/) ) <-> ( R Fr A /\ B C_ A /\ B =/= (/) ) ) )
11 raleq 
 |-  ( b = B -> ( A. y e. b -. y R x <-> A. y e. B -. y R x ) )
12 11 rexeqbi1dv 
 |-  ( b = B -> ( E. x e. b A. y e. b -. y R x <-> E. x e. B A. y e. B -. y R x ) )
13 10 12 imbi12d 
 |-  ( b = B -> ( ( ( R Fr A /\ b C_ A /\ b =/= (/) ) -> E. x e. b A. y e. b -. y R x ) <-> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
14 7 13 mpbii 
 |-  ( b = B -> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
15 3 14 bnj593 
 |-  ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. b ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
16 15 bnj937 
 |-  ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) )
17 1 16 mpd 
 |-  ( ( R Fr A /\ B C_ A /\ B =/= (/) /\ B e. _V ) -> E. x e. B A. y e. B -. y R x )