Metamath Proof Explorer


Theorem bnj544

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 bnj544.1 ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj544.2 ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑚 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj544.3 𝐷 = ( ω ∖ { ∅ } )
bnj544.4 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝑦 ∈ ( 𝑓𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
bnj544.5 ( 𝜏 ↔ ( 𝑓 Fn 𝑚𝜑′𝜓′ ) )
bnj544.6 ( 𝜎 ↔ ( 𝑚𝐷𝑛 = suc 𝑚𝑝𝑚 ) )
Assertion bnj544 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝐺 Fn 𝑛 )

Proof

Step Hyp Ref Expression
1 bnj544.1 ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj544.2 ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑚 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj544.3 𝐷 = ( ω ∖ { ∅ } )
4 bnj544.4 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝑦 ∈ ( 𝑓𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
5 bnj544.5 ( 𝜏 ↔ ( 𝑓 Fn 𝑚𝜑′𝜓′ ) )
6 bnj544.6 ( 𝜎 ↔ ( 𝑚𝐷𝑛 = suc 𝑚𝑝𝑚 ) )
7 3 bnj923 ( 𝑚𝐷𝑚 ∈ ω )
8 7 3anim1i ( ( 𝑚𝐷𝑛 = suc 𝑚𝑝𝑚 ) → ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝𝑚 ) )
9 6 8 sylbi ( 𝜎 → ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝𝑚 ) )
10 biid ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝𝑚 ) ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝𝑚 ) )
11 1 2 4 5 10 bnj543 ( ( 𝑅 FrSe 𝐴𝜏 ∧ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝𝑚 ) ) → 𝐺 Fn 𝑛 )
12 9 11 syl3an3 ( ( 𝑅 FrSe 𝐴𝜏𝜎 ) → 𝐺 Fn 𝑛 )