Metamath Proof Explorer


Theorem bnj1006

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 bnj1006.1 φf=predXAR
bnj1006.2 ψiωsucinfsuci=yfipredyAR
bnj1006.3 χnDfFnnφψ
bnj1006.4 θRFrSeAXAytrClXARzpredyAR
bnj1006.5 τmωn=sucmp=sucn
bnj1006.6 ηinyfi
bnj1006.7 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj1006.8 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj1006.9 No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
bnj1006.10 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj1006.11 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj1006.12 No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
bnj1006.13 D=ω
bnj1006.15 C=yfmpredyAR
bnj1006.16 G=fnC
bnj1006.28 No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
Assertion bnj1006 θχτηpredyARGsuci

Proof

Step Hyp Ref Expression
1 bnj1006.1 φf=predXAR
2 bnj1006.2 ψiωsucinfsuci=yfipredyAR
3 bnj1006.3 χnDfFnnφψ
4 bnj1006.4 θRFrSeAXAytrClXARzpredyAR
5 bnj1006.5 τmωn=sucmp=sucn
6 bnj1006.6 ηinyfi
7 bnj1006.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
8 bnj1006.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
9 bnj1006.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
10 bnj1006.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
11 bnj1006.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
12 bnj1006.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
13 bnj1006.13 D=ω
14 bnj1006.15 C=yfmpredyAR
15 bnj1006.16 G=fnC
16 bnj1006.28 Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
17 6 simprbi ηyfi
18 17 bnj708 θχτηyfi
19 bnj253 RFrSeAXAytrClXARzpredyARRFrSeAXAytrClXARzpredyAR
20 19 simp1bi RFrSeAXAytrClXARzpredyARRFrSeAXA
21 4 20 sylbi θRFrSeAXA
22 21 bnj705 θχτηRFrSeAXA
23 bnj643 θχτηχ
24 3simpc mωn=sucmp=sucnn=sucmp=sucn
25 5 24 sylbi τn=sucmp=sucn
26 25 bnj707 θχτηn=sucmp=sucn
27 3anass χn=sucmp=sucnχn=sucmp=sucn
28 23 26 27 sylanbrc θχτηχn=sucmp=sucn
29 biid fFnnφψfFnnφψ
30 biid nDp=sucnmnnDp=sucnmn
31 1 2 3 13 14 29 30 bnj969 RFrSeAXAχn=sucmp=sucnCV
32 22 28 31 syl2anc θχτηCV
33 3 bnj1235 χfFnn
34 33 bnj706 θχτηfFnn
35 5 simp3bi τp=sucn
36 35 bnj707 θχτηp=sucn
37 6 simplbi ηin
38 37 bnj708 θχτηin
39 32 34 36 38 bnj951 θχτηCVfFnnp=sucnin
40 15 bnj945 CVfFnnp=sucninGi=fi
41 39 40 syl θχτηGi=fi
42 18 41 eleqtrrd θχτηyGi
43 16 anim1i Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) with typecode |-
44 df-bnj17 Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) with typecode |-
45 43 44 sylibr Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) with typecode |-
46 1 2 3 7 8 9 10 11 12 14 15 bnj999 Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode |-
47 45 46 syl θχτηyGipredyARGsuci
48 42 47 mpdan θχτηpredyARGsuci