Metamath Proof Explorer

Theorem bnj1190

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1190.1 
|- ( ph <-> ( R _FrSe A /\ B C_ A /\ B =/= (/) ) )
bnj1190.2 
|- ( ps <-> ( x e. B /\ y e. B /\ y R x ) )
Assertion bnj1190 
|- ( ( ph /\ ps ) -> E. w e. B A. z e. B -. z R w )

Proof

Step Hyp Ref Expression
1 bnj1190.1 
 |-  ( ph <-> ( R _FrSe A /\ B C_ A /\ B =/= (/) ) )
2 bnj1190.2 
 |-  ( ps <-> ( x e. B /\ y e. B /\ y R x ) )
3 1 simp2bi 
 |-  ( ph -> B C_ A )
4 3 adantr 
 |-  ( ( ph /\ ps ) -> B C_ A )
5 eqid 
 |-  ( _trCl ( x , A , R ) i^i B ) = ( _trCl ( x , A , R ) i^i B )
6 1 simp1bi 
 |-  ( ph -> R _FrSe A )
7 6 adantr 
 |-  ( ( ph /\ ps ) -> R _FrSe A )
8 2 simp1bi 
 |-  ( ps -> x e. B )
9 ssel2 
 |-  ( ( B C_ A /\ x e. B ) -> x e. A )
10 3 8 9 syl2an 
 |-  ( ( ph /\ ps ) -> x e. A )
11 2 5 7 4 10 bnj1177 
 |-  ( ( ph /\ ps ) -> ( R Fr A /\ ( _trCl ( x , A , R ) i^i B ) C_ A /\ ( _trCl ( x , A , R ) i^i B ) =/= (/) /\ ( _trCl ( x , A , R ) i^i B ) e. _V ) )
12 bnj1154 
 |-  ( ( R Fr A /\ ( _trCl ( x , A , R ) i^i B ) C_ A /\ ( _trCl ( x , A , R ) i^i B ) =/= (/) /\ ( _trCl ( x , A , R ) i^i B ) e. _V ) -> E. u e. ( _trCl ( x , A , R ) i^i B ) A. v e. ( _trCl ( x , A , R ) i^i B ) -. v R u )
13 11 12 bnj1176 
 |-  E. u A. v ( ( ph /\ ps ) -> ( u e. ( _trCl ( x , A , R ) i^i B ) /\ ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) -> ( v R u -> -. v e. ( _trCl ( x , A , R ) i^i B ) ) ) ) )
14 biid 
 |-  ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ ( v e. A /\ v R u ) ) <-> ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ ( v e. A /\ v R u ) ) )
15 biid 
 |-  ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) <-> ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) )
16 5 14 15 bnj1175 
 |-  ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) -> ( v R u -> v e. _trCl ( x , A , R ) ) )
17 5 13 16 bnj1174 
 |-  E. u A. v ( ( ph /\ ps ) -> ( ( ph /\ ps /\ u e. ( _trCl ( x , A , R ) i^i B ) ) /\ ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) -> ( v R u -> -. v e. B ) ) ) )
18 5 15 7 10 bnj1173 
 |-  ( ( ph /\ ps /\ u e. ( _trCl ( x , A , R ) i^i B ) ) -> ( ( ( R _FrSe A /\ x e. A /\ u e. _trCl ( x , A , R ) ) /\ ( R _FrSe A /\ u e. A ) /\ v e. A ) <-> v e. A ) )
19 5 17 18 bnj1172 
 |-  E. u A. v ( ( ph /\ ps ) -> ( u e. B /\ ( v e. A -> ( v R u -> -. v e. B ) ) ) )
20 4 19 bnj1171 
 |-  E. u A. v ( ( ph /\ ps ) -> ( u e. B /\ ( v e. B -> -. v R u ) ) )
21 20 bnj1186 
 |-  ( ( ph /\ ps ) -> E. u e. B A. v e. B -. v R u )
22 21 bnj1185 
 |-  ( ( ph /\ ps ) -> E. x e. B A. y e. B -. y R x )
23 22 bnj1185 
 |-  ( ( ph /\ ps ) -> E. w e. B A. z e. B -. z R w )