Metamath Proof Explorer


Theorem bnj1033

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 bnj1033.1 φ f = pred X A R
bnj1033.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj1033.3 χ n D f Fn n φ ψ
bnj1033.4 θ R FrSe A X A
bnj1033.5 τ B V TrFo B A R pred X A R B
bnj1033.6 η z trCl X A R
bnj1033.7 ζ i n z f i
bnj1033.8 D = ω
bnj1033.9 K = f | n D f Fn n φ ψ
bnj1033.10 f n i θ τ χ ζ z B
Assertion bnj1033 θ τ trCl X A R B

Proof

Step Hyp Ref Expression
1 bnj1033.1 φ f = pred X A R
2 bnj1033.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj1033.3 χ n D f Fn n φ ψ
4 bnj1033.4 θ R FrSe A X A
5 bnj1033.5 τ B V TrFo B A R pred X A R B
6 bnj1033.6 η z trCl X A R
7 bnj1033.7 ζ i n z f i
8 bnj1033.8 D = ω
9 bnj1033.9 K = f | n D f Fn n φ ψ
10 bnj1033.10 f n i θ τ χ ζ z B
11 1 2 8 9 3 bnj983 z trCl X A R f n i χ i n z f i
12 19.42v i θ τ χ i n z f i θ τ i χ i n z f i
13 df-3an θ τ χ i n z f i θ τ χ i n z f i
14 13 exbii i θ τ χ i n z f i i θ τ χ i n z f i
15 df-3an θ τ i χ i n z f i θ τ i χ i n z f i
16 12 14 15 3bitr4i i θ τ χ i n z f i θ τ i χ i n z f i
17 16 exbii n i θ τ χ i n z f i n θ τ i χ i n z f i
18 19.42v n θ τ i χ i n z f i θ τ n i χ i n z f i
19 15 exbii n θ τ i χ i n z f i n θ τ i χ i n z f i
20 df-3an θ τ n i χ i n z f i θ τ n i χ i n z f i
21 18 19 20 3bitr4i n θ τ i χ i n z f i θ τ n i χ i n z f i
22 17 21 bitri n i θ τ χ i n z f i θ τ n i χ i n z f i
23 22 exbii f n i θ τ χ i n z f i f θ τ n i χ i n z f i
24 19.42v f θ τ n i χ i n z f i θ τ f n i χ i n z f i
25 20 exbii f θ τ n i χ i n z f i f θ τ n i χ i n z f i
26 df-3an θ τ f n i χ i n z f i θ τ f n i χ i n z f i
27 24 25 26 3bitr4i f θ τ n i χ i n z f i θ τ f n i χ i n z f i
28 23 27 bitri f n i θ τ χ i n z f i θ τ f n i χ i n z f i
29 bnj255 θ τ χ ζ θ τ χ ζ
30 7 anbi2i χ ζ χ i n z f i
31 3anass χ i n z f i χ i n z f i
32 30 31 bitr4i χ ζ χ i n z f i
33 32 3anbi3i θ τ χ ζ θ τ χ i n z f i
34 29 33 bitri θ τ χ ζ θ τ χ i n z f i
35 34 3exbii f n i θ τ χ ζ f n i θ τ χ i n z f i
36 35 10 sylbir f n i θ τ χ i n z f i z B
37 28 36 sylbir θ τ f n i χ i n z f i z B
38 11 37 syl3an3b θ τ z trCl X A R z B
39 38 3expia θ τ z trCl X A R z B
40 39 ssrdv θ τ trCl X A R B