Metamath Proof Explorer


Theorem bnj229

Description: Technical lemma for bnj517 . 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
Hypothesis bnj229.1 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑁 → ( 𝐹 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐹𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
Assertion bnj229 ( ( 𝑛𝑁 ∧ ( suc 𝑚 = 𝑛𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹𝑛 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 bnj229.1 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑁 → ( 𝐹 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐹𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj213 pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
3 2 bnj226 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
4 1 bnj222 ( 𝜓 ↔ ∀ 𝑚 ∈ ω ( suc 𝑚𝑁 → ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5 4 bnj228 ( ( 𝑚 ∈ ω ∧ 𝜓 ) → ( suc 𝑚𝑁 → ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6 5 adantl ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( suc 𝑚𝑁 → ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
7 eleq1 ( suc 𝑚 = 𝑛 → ( suc 𝑚𝑁𝑛𝑁 ) )
8 fveqeq2 ( suc 𝑚 = 𝑛 → ( ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
9 7 8 imbi12d ( suc 𝑚 = 𝑛 → ( ( suc 𝑚𝑁 → ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛𝑁 → ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
10 9 adantr ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( ( suc 𝑚𝑁 → ( 𝐹 ‘ suc 𝑚 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛𝑁 → ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
11 6 10 mpbid ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝑛𝑁 → ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
12 11 3impb ( ( suc 𝑚 = 𝑛𝑚 ∈ ω ∧ 𝜓 ) → ( 𝑛𝑁 → ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13 12 impcom ( ( 𝑛𝑁 ∧ ( suc 𝑚 = 𝑛𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹𝑛 ) = 𝑦 ∈ ( 𝐹𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14 3 13 bnj1262 ( ( 𝑛𝑁 ∧ ( suc 𝑚 = 𝑛𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹𝑛 ) ⊆ 𝐴 )