Description: Technical lemma for bnj150 . 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) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bnj96.1 | |- F = { <. (/) , _pred ( x , A , R ) >. } |
|
Assertion | bnj96 | |- ( ( R _FrSe A /\ x e. A ) -> dom F = 1o ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj96.1 | |- F = { <. (/) , _pred ( x , A , R ) >. } |
|
2 | bnj93 | |- ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V ) |
|
3 | dmsnopg | |- ( _pred ( x , A , R ) e. _V -> dom { <. (/) , _pred ( x , A , R ) >. } = { (/) } ) |
|
4 | 2 3 | syl | |- ( ( R _FrSe A /\ x e. A ) -> dom { <. (/) , _pred ( x , A , R ) >. } = { (/) } ) |
5 | 1 | dmeqi | |- dom F = dom { <. (/) , _pred ( x , A , R ) >. } |
6 | df1o2 | |- 1o = { (/) } |
|
7 | 4 5 6 | 3eqtr4g | |- ( ( R _FrSe A /\ x e. A ) -> dom F = 1o ) |