Metamath Proof Explorer

Theorem bnj557

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 bnj557.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj557.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
bnj557.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
bnj557.18 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
bnj557.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
bnj557.20 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
bnj557.21 ⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj557.22 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj557.23 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj557.24 ⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj557.25 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
bnj557.28 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj557.29 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj557.36 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
Assertion bnj557 ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )

Proof

Step Hyp Ref Expression
1 bnj557.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
2 bnj557.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
3 bnj557.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
4 bnj557.18 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
5 bnj557.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
6 bnj557.20 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
7 bnj557.21 ⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
8 bnj557.22 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
9 bnj557.23 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
10 bnj557.24 ⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
11 bnj557.25 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
12 bnj557.28 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13 bnj557.29 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
14 bnj557.36 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
15 3an4anass ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
16 4 5 bnj556 ⊢ ( 𝜂 → 𝜎 )
17 16 3anim3i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) )
18 vex ⊢ 𝑖 ∈ V
19 18 bnj216 ⊢ ( 𝑚 = suc 𝑖 → 𝑖 ∈ 𝑚 )
20 6 19 bnj837 ⊢ ( 𝜁 → 𝑖 ∈ 𝑚 )
21 17 20 anim12i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) )
22 15 21 sylbir ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) )
23 5 bnj1254 ⊢ ( 𝜂 → 𝑚 = suc 𝑝 )
24 6 simp3bi ⊢ ( 𝜁 → 𝑚 = suc 𝑖 )
25 bnj551 ⊢ ( ( 𝑚 = suc 𝑝 ∧ 𝑚 = suc 𝑖 ) → 𝑝 = 𝑖 )
26 23 24 25 syl2an ⊢ ( ( 𝜂 ∧ 𝜁 ) → 𝑝 = 𝑖 )
27 26 adantl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → 𝑝 = 𝑖 )
28 22 27 jca ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) ∧ 𝑝 = 𝑖 ) )
29 bnj256 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
30 df-3an ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) ∧ 𝑝 = 𝑖 ) )
31 28 29 30 3imtr4i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) )
32 12 13 1 2 3 4 8 11 7 9 10 14 bnj553 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )
33 31 32 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝐺 ‘ 𝑚 ) = 𝐿 )