Metamath Proof Explorer


Theorem bnj964

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 bnj964.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj964.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
bnj964.5 ( 𝜓′[ 𝑝 / 𝑛 ] 𝜓 )
bnj964.8 ( 𝜓″[ 𝐺 / 𝑓 ] 𝜓′ )
bnj964.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj964.13 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
bnj964.96 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
bnj964.165 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
Assertion bnj964 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜓″ )

Proof

Step Hyp Ref Expression
1 bnj964.2 ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑛 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj964.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
3 bnj964.5 ( 𝜓′[ 𝑝 / 𝑛 ] 𝜓 )
4 bnj964.8 ( 𝜓″[ 𝐺 / 𝑓 ] 𝜓′ )
5 bnj964.12 𝐶 = 𝑦 ∈ ( 𝑓𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
6 bnj964.13 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
7 bnj964.96 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
8 bnj964.165 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
9 nfv 𝑖 ( 𝑅 FrSe 𝐴𝑋𝐴 )
10 1 bnj1095 ( 𝜓 → ∀ 𝑖 𝜓 )
11 10 2 bnj1096 ( 𝜒 → ∀ 𝑖 𝜒 )
12 11 nf5i 𝑖 𝜒
13 nfv 𝑖 𝑛 = suc 𝑚
14 nfv 𝑖 𝑝 = suc 𝑛
15 12 13 14 nf3an 𝑖 ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 )
16 9 15 nfan 𝑖 ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) )
17 bnj255 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) )
18 bnj645 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → suc 𝑖𝑝 )
19 simp3 ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → 𝑝 = suc 𝑛 )
20 19 bnj706 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → 𝑝 = suc 𝑛 )
21 eleq2 ( 𝑝 = suc 𝑛 → ( suc 𝑖𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) )
22 21 biimpac ( ( suc 𝑖𝑝𝑝 = suc 𝑛 ) → suc 𝑖 ∈ suc 𝑛 )
23 elsuci ( suc 𝑖 ∈ suc 𝑛 → ( suc 𝑖𝑛 ∨ suc 𝑖 = 𝑛 ) )
24 eqcom ( suc 𝑖 = 𝑛𝑛 = suc 𝑖 )
25 24 orbi2i ( ( suc 𝑖𝑛 ∨ suc 𝑖 = 𝑛 ) ↔ ( suc 𝑖𝑛𝑛 = suc 𝑖 ) )
26 23 25 sylib ( suc 𝑖 ∈ suc 𝑛 → ( suc 𝑖𝑛𝑛 = suc 𝑖 ) )
27 22 26 syl ( ( suc 𝑖𝑝𝑝 = suc 𝑛 ) → ( suc 𝑖𝑛𝑛 = suc 𝑖 ) )
28 18 20 27 syl2anc ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( suc 𝑖𝑛𝑛 = suc 𝑖 ) )
29 df-3an ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) )
30 29 3anbi3i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) ) )
31 bnj255 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) ) )
32 30 31 bitr4i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) )
33 bnj345 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ suc 𝑖𝑛 ) ↔ ( suc 𝑖𝑛 ∧ ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) )
34 bnj252 ( ( suc 𝑖𝑛 ∧ ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ↔ ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
35 32 33 34 3bitri ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) ↔ ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
36 17 anbi2i ( ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ↔ ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
37 35 36 bitr4i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ∧ suc 𝑖𝑛 ) ) ↔ ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) )
38 37 7 sylbir ( ( suc 𝑖𝑛 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
39 38 ex ( suc 𝑖𝑛 → ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
40 df-3an ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) )
41 40 3anbi3i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) )
42 bnj255 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) )
43 41 42 bitr4i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) ↔ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) )
44 bnj345 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ∧ 𝑛 = suc 𝑖 ) ↔ ( 𝑛 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) )
45 bnj252 ( ( 𝑛 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
46 43 44 45 3bitri ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
47 17 anbi2i ( ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) ) )
48 46 47 bitr4i ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝𝑛 = suc 𝑖 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) )
49 48 8 sylbir ( ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
50 49 ex ( 𝑛 = suc 𝑖 → ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
51 39 50 jaoi ( ( suc 𝑖𝑛𝑛 = suc 𝑖 ) → ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
52 28 51 mpcom ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
53 17 52 sylbir ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
54 53 3expia ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
55 16 54 alrimi ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
56 vex 𝑝 ∈ V
57 1 3 56 bnj539 ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑝 → ( 𝑓 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝑓𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
58 57 4 5 6 bnj965 ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖𝑝 → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
59 58 bnj115 ( 𝜓″ ↔ ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝑦 ∈ ( 𝐺𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
60 55 59 sylibr ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝜓″ )