Metamath Proof Explorer


Theorem bnj1128

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 bnj1128.1 φ f = pred X A R
bnj1128.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj1128.3 D = ω
bnj1128.4 B = f | n D f Fn n φ ψ
bnj1128.5 χ n D f Fn n φ ψ
bnj1128.6 θ χ f i A
bnj1128.7 τ j n j E i [˙j / i]˙ θ
bnj1128.8 No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |-
bnj1128.9 No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |-
bnj1128.10 No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |-
bnj1128.11 No typesetting found for |- ( th' <-> [. j / i ]. th ) with typecode |-
Assertion bnj1128 Y trCl X A R Y A

Proof

Step Hyp Ref Expression
1 bnj1128.1 φ f = pred X A R
2 bnj1128.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj1128.3 D = ω
4 bnj1128.4 B = f | n D f Fn n φ ψ
5 bnj1128.5 χ n D f Fn n φ ψ
6 bnj1128.6 θ χ f i A
7 bnj1128.7 τ j n j E i [˙j / i]˙ θ
8 bnj1128.8 Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |-
9 bnj1128.9 Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |-
10 bnj1128.10 Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |-
11 bnj1128.11 Could not format ( th' <-> [. j / i ]. th ) : No typesetting found for |- ( th' <-> [. j / i ]. th ) with typecode |-
12 1 2 3 4 5 bnj981 Y trCl X A R f n i χ i n Y f i
13 simp1 χ i n Y f i χ
14 simp2 χ i n Y f i i n
15 nfv j i n
16 nfra1 j j n j E i [˙j / i]˙ θ
17 7 16 nfxfr j τ
18 nfv j χ
19 15 17 18 nf3an j i n τ χ
20 nfv j f i A
21 19 20 nfim j i n τ χ f i A
22 21 nf5ri i n τ χ f i A j i n τ χ f i A
23 3 bnj1098 j i i n n D j n i = suc j
24 simpl i i n τ χ i
25 simpr1 i i n τ χ i n
26 5 bnj1232 χ n D
27 26 3ad2ant3 i n τ χ n D
28 27 adantl i i n τ χ n D
29 24 25 28 3jca i i n τ χ i i n n D
30 23 29 bnj1101 j i i n τ χ j n i = suc j
31 ancl i i n τ χ j n i = suc j i i n τ χ i i n τ χ j n i = suc j
32 30 31 bnj101 j i i n τ χ i i n τ χ j n i = suc j
33 df-3an i i n τ χ j n i = suc j i i n τ χ j n i = suc j
34 33 imbi2i i i n τ χ i i n τ χ j n i = suc j i i n τ χ i i n τ χ j n i = suc j
35 34 exbii j i i n τ χ i i n τ χ j n i = suc j j i i n τ χ i i n τ χ j n i = suc j
36 32 35 mpbir j i i n τ χ i i n τ χ j n i = suc j
37 bnj213 pred y A R A
38 37 bnj226 y f j pred y A R A
39 simp21 i i n τ χ j n i = suc j i n
40 simp3r i i n τ χ j n i = suc j i = suc j
41 biid n D n D
42 biid f Fn n f Fn n
43 vex j V
44 sbcg j V [˙j / i]˙ φ φ
45 43 44 ax-mp [˙j / i]˙ φ φ
46 8 45 bitr2i Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |-
47 2 9 bnj1039 Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
48 2 47 bitr4i Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |-
49 41 42 46 48 bnj887 Could not format ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |-
50 8 9 5 10 bnj1040 Could not format ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |-
51 49 5 50 3bitr4i Could not format ( ch <-> ch' ) : No typesetting found for |- ( ch <-> ch' ) with typecode |-
52 50 bnj1254 Could not format ( ch' -> ps' ) : No typesetting found for |- ( ch' -> ps' ) with typecode |-
53 51 52 sylbi Could not format ( ch -> ps' ) : No typesetting found for |- ( ch -> ps' ) with typecode |-
54 53 3ad2ant3 Could not format ( ( i e. n /\ ta /\ ch ) -> ps' ) : No typesetting found for |- ( ( i e. n /\ ta /\ ch ) -> ps' ) with typecode |-
55 54 3ad2ant2 Could not format ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) : No typesetting found for |- ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' ) with typecode |-
56 simp3l i i n τ χ j n i = suc j j n
57 27 3ad2ant2 i i n τ χ j n i = suc j n D
58 3 bnj923 n D n ω
59 elnn j n n ω j ω
60 58 59 sylan2 j n n D j ω
61 56 57 60 syl2anc i i n τ χ j n i = suc j j ω
62 47 bnj589 Could not format ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) with typecode |-
63 rsp j ω suc j n f suc j = y f j pred y A R j ω suc j n f suc j = y f j pred y A R
64 62 63 sylbi Could not format ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) : No typesetting found for |- ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) with typecode |-
65 eleq1 i = suc j i n suc j n
66 fveqeq2 i = suc j f i = y f j pred y A R f suc j = y f j pred y A R
67 65 66 imbi12d i = suc j i n f i = y f j pred y A R suc j n f suc j = y f j pred y A R
68 67 imbi2d i = suc j j ω i n f i = y f j pred y A R j ω suc j n f suc j = y f j pred y A R
69 64 68 syl5ibr Could not format ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) : No typesetting found for |- ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) ) with typecode |-
70 40 55 61 69 syl3c i i n τ χ j n i = suc j i n f i = y f j pred y A R
71 39 70 mpd i i n τ χ j n i = suc j f i = y f j pred y A R
72 38 71 bnj1262 i i n τ χ j n i = suc j f i A
73 36 72 bnj1023 j i i n τ χ f i A
74 5 bnj1247 χ φ
75 74 3ad2ant3 i n τ χ φ
76 bnj213 pred X A R A
77 fveq2 i = f i = f
78 1 biimpi φ f = pred X A R
79 77 78 sylan9eq i = φ f i = pred X A R
80 76 79 bnj1262 i = φ f i A
81 75 80 sylan2 i = i n τ χ f i A
82 73 81 bnj1109 j i n τ χ f i A
83 22 82 bnj1131 i n τ χ f i A
84 83 3expia i n τ χ f i A
85 84 6 sylibr i n τ θ
86 3 5 7 85 bnj1133 χ i n θ
87 6 ralbii i n θ i n χ f i A
88 86 87 sylib χ i n χ f i A
89 rsp i n χ f i A i n χ f i A
90 88 89 syl χ i n χ f i A
91 13 14 13 90 syl3c χ i n Y f i f i A
92 simp3 χ i n Y f i Y f i
93 91 92 sseldd χ i n Y f i Y A
94 93 2eximi n i χ i n Y f i n i Y A
95 12 94 bnj593 Y trCl X A R f n i Y A
96 19.9v f n i Y A n i Y A
97 19.9v n i Y A i Y A
98 19.9v i Y A Y A
99 96 97 98 3bitri f n i Y A Y A
100 95 99 sylib Y trCl X A R Y A