Metamath Proof Explorer


Theorem bnj1374

Description: Technical lemma for bnj60 . 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 bnj1374.1 B = d | d A x d pred x A R d
bnj1374.2 Y = x f pred x A R
bnj1374.3 C = f | d B f Fn d x d f x = G Y
bnj1374.4 τ f C dom f = x trCl x A R
bnj1374.5 D = x A | ¬ f τ
bnj1374.6 ψ R FrSe A D
bnj1374.7 χ ψ x D y D ¬ y R x
bnj1374.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1374.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
Assertion bnj1374 f H f C

Proof

Step Hyp Ref Expression
1 bnj1374.1 B = d | d A x d pred x A R d
2 bnj1374.2 Y = x f pred x A R
3 bnj1374.3 C = f | d B f Fn d x d f x = G Y
4 bnj1374.4 τ f C dom f = x trCl x A R
5 bnj1374.5 D = x A | ¬ f τ
6 bnj1374.6 ψ R FrSe A D
7 bnj1374.7 χ ψ x D y D ¬ y R x
8 bnj1374.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1374.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 9 bnj1436 Could not format ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for |- ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) with typecode |-
11 rexex Could not format ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) : No typesetting found for |- ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) with typecode |-
12 10 11 syl Could not format ( f e. H -> E. y ta' ) : No typesetting found for |- ( f e. H -> E. y ta' ) with typecode |-
13 1 2 3 4 8 bnj1373 Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
14 13 exbii Could not format ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
15 12 14 sylib f H y f C dom f = y trCl y A R
16 exsimpl y f C dom f = y trCl y A R y f C
17 15 16 syl f H y f C
18 17 bnj937 f H f C