Metamath Proof Explorer


Theorem bnj910

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 bnj910.1 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj910.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj910.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
bnj910.4 ( 𝜑′[ 𝑝 / 𝑛 ] 𝜑 )
bnj910.5 ( 𝜓′[ 𝑝 / 𝑛 ] 𝜓 )
bnj910.6 ( 𝜒′[ 𝑝 / 𝑛 ] 𝜒 )
bnj910.7 ( 𝜑″[ 𝐺 / 𝑓 ] 𝜑′ )
bnj910.8 ( 𝜓″[ 𝐺 / 𝑓 ] 𝜓′ )
bnj910.9 ( 𝜒″[ 𝐺 / 𝑓 ] 𝜒′ )
bnj910.10 𝐷 = ( ω ∖ { ∅ } )
bnj910.11 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
bnj910.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj910.13 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
bnj910.14 ( 𝜏 ↔ ( 𝑓 Fn 𝑛𝜑𝜓 ) )
bnj910.15 ( 𝜎 ↔ ( 𝑛𝐷𝑝 = suc 𝑛𝑚𝑛 ) )
Assertion bnj910 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜒″ )

Proof

Step Hyp Ref Expression
1 bnj910.1 ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj910.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj910.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
4 bnj910.4 ( 𝜑′[ 𝑝 / 𝑛 ] 𝜑 )
5 bnj910.5 ( 𝜓′[ 𝑝 / 𝑛 ] 𝜓 )
6 bnj910.6 ( 𝜒′[ 𝑝 / 𝑛 ] 𝜒 )
7 bnj910.7 ( 𝜑″[ 𝐺 / 𝑓 ] 𝜑′ )
8 bnj910.8 ( 𝜓″[ 𝐺 / 𝑓 ] 𝜓′ )
9 bnj910.9 ( 𝜒″[ 𝐺 / 𝑓 ] 𝜒′ )
10 bnj910.10 𝐷 = ( ω ∖ { ∅ } )
11 bnj910.11 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
12 bnj910.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
13 bnj910.13 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
14 bnj910.14 ( 𝜏 ↔ ( 𝑓 Fn 𝑛𝜑𝜓 ) )
15 bnj910.15 ( 𝜎 ↔ ( 𝑛𝐷𝑝 = suc 𝑛𝑚𝑛 ) )
16 3 10 bnj970 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑝𝐷 )
17 1 2 3 10 12 14 15 bnj969 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
18 simpr3 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑝 = suc 𝑛 )
19 3 bnj1235 ( 𝜒𝑓 Fn 𝑛 )
20 19 3ad2ant1 ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 )
21 20 adantl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑓 Fn 𝑛 )
22 13 bnj941 ( 𝐶 ∈ V → ( ( 𝑝 = suc 𝑛𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) )
23 22 3impib ( ( 𝐶 ∈ V ∧ 𝑝 = suc 𝑛𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 )
24 17 18 21 23 syl3anc ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝐺 Fn 𝑝 )
25 1 2 3 4 7 10 12 13 14 15 bnj944 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜑″ )
26 2 3 10 12 13 17 bnj967 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
27 3 10 12 13 17 24 bnj966 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
28 2 3 5 8 12 13 26 27 bnj964 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜓″ )
29 16 24 25 28 bnj951 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ( 𝑝𝐷𝐺 Fn 𝑝𝜑″𝜓″ ) )
30 vex 𝑝 ∈ V
31 3 4 5 6 30 bnj919 ( 𝜒′ ↔ ( 𝑝𝐷𝑓 Fn 𝑝𝜑′𝜓′ ) )
32 13 bnj918 𝐺 ∈ V
33 31 7 8 9 32 bnj976 ( 𝜒″ ↔ ( 𝑝𝐷𝐺 Fn 𝑝𝜑″𝜓″ ) )
34 29 33 sylibr ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜒″ )