Metamath Proof Explorer

Theorem bnj1177

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 bnj1177.2 
|- ( ps <-> ( X e. B /\ y e. B /\ y R X ) )
bnj1177.3 
|- C = ( _trCl ( X , A , R ) i^i B )
bnj1177.9 
|- ( ( ph /\ ps ) -> R _FrSe A )
bnj1177.13 
|- ( ( ph /\ ps ) -> B C_ A )
bnj1177.17 
|- ( ( ph /\ ps ) -> X e. A )
Assertion bnj1177 
|- ( ( ph /\ ps ) -> ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) )

Proof

Step Hyp Ref Expression
1 bnj1177.2 
 |-  ( ps <-> ( X e. B /\ y e. B /\ y R X ) )
2 bnj1177.3 
 |-  C = ( _trCl ( X , A , R ) i^i B )
3 bnj1177.9 
 |-  ( ( ph /\ ps ) -> R _FrSe A )
4 bnj1177.13 
 |-  ( ( ph /\ ps ) -> B C_ A )
5 bnj1177.17 
 |-  ( ( ph /\ ps ) -> X e. A )
6 df-bnj15 
 |-  ( R _FrSe A <-> ( R Fr A /\ R _Se A ) )
7 6 simplbi 
 |-  ( R _FrSe A -> R Fr A )
8 3 7 syl 
 |-  ( ( ph /\ ps ) -> R Fr A )
9 bnj1147 
 |-  _trCl ( X , A , R ) C_ A
10 ssinss1 
 |-  ( _trCl ( X , A , R ) C_ A -> ( _trCl ( X , A , R ) i^i B ) C_ A )
11 9 10 ax-mp 
 |-  ( _trCl ( X , A , R ) i^i B ) C_ A
12 2 11 eqsstri 
 |-  C C_ A
13 12 a1i 
 |-  ( ( ph /\ ps ) -> C C_ A )
14 bnj906 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
15 3 5 14 syl2anc 
 |-  ( ( ph /\ ps ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
16 15 ssrind 
 |-  ( ( ph /\ ps ) -> ( _pred ( X , A , R ) i^i B ) C_ ( _trCl ( X , A , R ) i^i B ) )
17 1 simp2bi 
 |-  ( ps -> y e. B )
18 17 adantl 
 |-  ( ( ph /\ ps ) -> y e. B )
19 4 18 sseldd 
 |-  ( ( ph /\ ps ) -> y e. A )
20 1 simp3bi 
 |-  ( ps -> y R X )
21 20 adantl 
 |-  ( ( ph /\ ps ) -> y R X )
22 bnj1152 
 |-  ( y e. _pred ( X , A , R ) <-> ( y e. A /\ y R X ) )
23 19 21 22 sylanbrc 
 |-  ( ( ph /\ ps ) -> y e. _pred ( X , A , R ) )
24 23 18 elind 
 |-  ( ( ph /\ ps ) -> y e. ( _pred ( X , A , R ) i^i B ) )
25 16 24 sseldd 
 |-  ( ( ph /\ ps ) -> y e. ( _trCl ( X , A , R ) i^i B ) )
26 25 ne0d 
 |-  ( ( ph /\ ps ) -> ( _trCl ( X , A , R ) i^i B ) =/= (/) )
27 2 neeq1i 
 |-  ( C =/= (/) <-> ( _trCl ( X , A , R ) i^i B ) =/= (/) )
28 26 27 sylibr 
 |-  ( ( ph /\ ps ) -> C =/= (/) )
29 bnj893 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )
30 3 5 29 syl2anc 
 |-  ( ( ph /\ ps ) -> _trCl ( X , A , R ) e. _V )
31 inex1g 
 |-  ( _trCl ( X , A , R ) e. _V -> ( _trCl ( X , A , R ) i^i B ) e. _V )
32 2 31 eqeltrid 
 |-  ( _trCl ( X , A , R ) e. _V -> C e. _V )
33 30 32 syl 
 |-  ( ( ph /\ ps ) -> C e. _V )
34 8 13 28 33 bnj951 
 |-  ( ( ph /\ ps ) -> ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) )