Metamath Proof Explorer


Theorem bnj864

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 bnj864.1 φ f = pred X A R
bnj864.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj864.3 D = ω
bnj864.4 χ R FrSe A X A n D
bnj864.5 θ f Fn n φ ψ
Assertion bnj864 χ ∃! f θ

Proof

Step Hyp Ref Expression
1 bnj864.1 φ f = pred X A R
2 bnj864.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj864.3 D = ω
4 bnj864.4 χ R FrSe A X A n D
5 bnj864.5 θ f Fn n φ ψ
6 1 2 3 bnj852 R FrSe A X A n D ∃! f f Fn n φ ψ
7 df-ral n D ∃! f f Fn n φ ψ n n D ∃! f f Fn n φ ψ
8 7 imbi2i R FrSe A X A n D ∃! f f Fn n φ ψ R FrSe A X A n n D ∃! f f Fn n φ ψ
9 19.21v n R FrSe A X A n D ∃! f f Fn n φ ψ R FrSe A X A n n D ∃! f f Fn n φ ψ
10 impexp R FrSe A X A n D ∃! f f Fn n φ ψ R FrSe A X A n D ∃! f f Fn n φ ψ
11 df-3an R FrSe A X A n D R FrSe A X A n D
12 11 bicomi R FrSe A X A n D R FrSe A X A n D
13 12 imbi1i R FrSe A X A n D ∃! f f Fn n φ ψ R FrSe A X A n D ∃! f f Fn n φ ψ
14 10 13 bitr3i R FrSe A X A n D ∃! f f Fn n φ ψ R FrSe A X A n D ∃! f f Fn n φ ψ
15 14 albii n R FrSe A X A n D ∃! f f Fn n φ ψ n R FrSe A X A n D ∃! f f Fn n φ ψ
16 8 9 15 3bitr2i R FrSe A X A n D ∃! f f Fn n φ ψ n R FrSe A X A n D ∃! f f Fn n φ ψ
17 6 16 mpbi n R FrSe A X A n D ∃! f f Fn n φ ψ
18 17 spi R FrSe A X A n D ∃! f f Fn n φ ψ
19 5 eubii ∃! f θ ∃! f f Fn n φ ψ
20 18 4 19 3imtr4i χ ∃! f θ