Metamath Proof Explorer


Theorem bnj153

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 bnj153.1 φ f = pred x A R
bnj153.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj153.3 D = ω
bnj153.4 θ R FrSe A x A ∃! f f Fn n φ ψ
bnj153.5 τ m D m E n [˙m / n]˙ θ
Assertion bnj153 n = 1 𝑜 n D τ θ

Proof

Step Hyp Ref Expression
1 bnj153.1 φ f = pred x A R
2 bnj153.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj153.3 D = ω
4 bnj153.4 θ R FrSe A x A ∃! f f Fn n φ ψ
5 bnj153.5 τ m D m E n [˙m / n]˙ θ
6 biid R FrSe A x A f Fn n φ ψ R FrSe A x A f Fn n φ ψ
7 biid [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ φ
8 1 7 bnj118 [˙ 1 𝑜 / n]˙ φ f = pred x A R
9 8 bicomi f = pred x A R [˙ 1 𝑜 / n]˙ φ
10 bnj105 1 𝑜 V
11 2 10 bnj92 [˙ 1 𝑜 / n]˙ ψ i ω suc i 1 𝑜 f suc i = y f i pred y A R
12 11 bicomi i ω suc i 1 𝑜 f suc i = y f i pred y A R [˙ 1 𝑜 / n]˙ ψ
13 biid [˙ 1 𝑜 / n]˙ θ [˙ 1 𝑜 / n]˙ θ
14 biid R FrSe A x A f f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R R FrSe A x A f f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
15 biid R FrSe A x A * f f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R R FrSe A x A * f f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
16 biid [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ
17 biid [˙ 1 𝑜 / n]˙ ψ [˙ 1 𝑜 / n]˙ ψ
18 6 16 7 17 bnj121 [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ R FrSe A x A f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ
19 8 anbi2i f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ f Fn 1 𝑜 f = pred x A R
20 19 11 anbi12i f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
21 df-3an f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ
22 df-3an f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
23 20 21 22 3bitr4i f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
24 23 imbi2i R FrSe A x A f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ R FrSe A x A f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
25 18 24 bitri [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ R FrSe A x A f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
26 25 bicomi R FrSe A x A f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ
27 eqid pred x A R = pred x A R
28 biid [˙ pred x A R / f]˙ f = pred x A R [˙ pred x A R / f]˙ f = pred x A R
29 biid [˙ pred x A R / f]˙ i ω suc i 1 𝑜 f suc i = y f i pred y A R [˙ pred x A R / f]˙ i ω suc i 1 𝑜 f suc i = y f i pred y A R
30 26 sbcbii [˙ pred x A R / f]˙ R FrSe A x A f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ
31 biid [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ
32 biid [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ
33 biid [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ
34 27 31 32 33 18 bnj124 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ R FrSe A x A pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ
35 1 7 31 27 bnj125 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ pred x A R = pred x A R
36 35 anbi2i pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ pred x A R Fn 1 𝑜 pred x A R = pred x A R
37 2 17 32 27 bnj126 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
38 36 37 anbi12i pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
39 df-3an pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ
40 df-3an pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
41 38 39 40 3bitr4i pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
42 41 imbi2i R FrSe A x A pred x A R Fn 1 𝑜 [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ φ [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ ψ R FrSe A x A pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
43 34 42 bitri [˙ pred x A R / f]˙ [˙ 1 𝑜 / n]˙ R FrSe A x A f Fn n φ ψ R FrSe A x A pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R
44 30 43 bitr2i R FrSe A x A pred x A R Fn 1 𝑜 pred x A R = pred x A R i ω suc i 1 𝑜 pred x A R suc i = y pred x A R i pred y A R [˙ pred x A R / f]˙ R FrSe A x A f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
45 biid f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
46 biid f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ
47 biid [˙g / f]˙ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ [˙g / f]˙ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ
48 biid [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ
49 biid [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ
50 46 47 48 49 bnj156 [˙g / f]˙ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ
51 48 8 bnj154 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ g = pred x A R
52 51 anbi2i g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ g Fn 1 𝑜 g = pred x A R
53 17 11 bitri [˙ 1 𝑜 / n]˙ ψ i ω suc i 1 𝑜 f suc i = y f i pred y A R
54 49 53 bnj155 [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ i ω suc i 1 𝑜 g suc i = y g i pred y A R
55 52 54 anbi12i g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R
56 df-3an g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ
57 df-3an g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R
58 55 56 57 3bitr4i g Fn 1 𝑜 [˙g / f]˙ [˙ 1 𝑜 / n]˙ φ [˙g / f]˙ [˙ 1 𝑜 / n]˙ ψ g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R
59 50 58 bitri [˙g / f]˙ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R
60 23 sbcbii [˙g / f]˙ f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ [˙g / f]˙ f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
61 59 60 bitr3i g Fn 1 𝑜 g = pred x A R i ω suc i 1 𝑜 g suc i = y g i pred y A R [˙g / f]˙ f Fn 1 𝑜 f = pred x A R i ω suc i 1 𝑜 f suc i = y f i pred y A R
62 biid [˙g / f]˙ f = pred x A R [˙g / f]˙ f = pred x A R
63 biid [˙g / f]˙ i ω suc i 1 𝑜 f suc i = y f i pred y A R [˙g / f]˙ i ω suc i 1 𝑜 f suc i = y f i pred y A R
64 1 2 3 4 5 6 9 12 13 14 15 26 27 28 29 44 45 61 62 63 bnj151 n = 1 𝑜 n D τ θ