Metamath Proof Explorer


Theorem bnj535

Description: Technical lemma for bnj852 . 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 bnj535.1 No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj535.2 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
bnj535.3 G = f m y f p pred y A R
bnj535.4 No typesetting found for |- ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
Assertion bnj535 R FrSe A τ n = m m f Fn m G Fn n

Proof

Step Hyp Ref Expression
1 bnj535.1 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
2 bnj535.2 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
3 bnj535.3 G = f m y f p pred y A R
4 bnj535.4 Could not format ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
5 bnj422 R FrSe A τ n = m m f Fn m n = m m f Fn m R FrSe A τ
6 bnj251 n = m m f Fn m R FrSe A τ n = m m f Fn m R FrSe A τ
7 5 6 bitri R FrSe A τ n = m m f Fn m n = m m f Fn m R FrSe A τ
8 fvex f p V
9 1 2 4 bnj518 R FrSe A τ y f p pred y A R V
10 iunexg f p V y f p pred y A R V y f p pred y A R V
11 8 9 10 sylancr R FrSe A τ y f p pred y A R V
12 vex m V
13 12 bnj519 y f p pred y A R V Fun m y f p pred y A R
14 11 13 syl R FrSe A τ Fun m y f p pred y A R
15 dmsnopg y f p pred y A R V dom m y f p pred y A R = m
16 11 15 syl R FrSe A τ dom m y f p pred y A R = m
17 14 16 bnj1422 R FrSe A τ m y f p pred y A R Fn m
18 bnj521 m m =
19 fnun f Fn m m y f p pred y A R Fn m m m = f m y f p pred y A R Fn m m
20 18 19 mpan2 f Fn m m y f p pred y A R Fn m f m y f p pred y A R Fn m m
21 17 20 sylan2 f Fn m R FrSe A τ f m y f p pred y A R Fn m m
22 3 fneq1i G Fn m m f m y f p pred y A R Fn m m
23 21 22 sylibr f Fn m R FrSe A τ G Fn m m
24 fneq2 n = m m G Fn n G Fn m m
25 23 24 syl5ibr n = m m f Fn m R FrSe A τ G Fn n
26 25 imp n = m m f Fn m R FrSe A τ G Fn n
27 7 26 sylbi R FrSe A τ n = m m f Fn m G Fn n