Metamath Proof Explorer

Theorem bnj571

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

Proof

Step Hyp Ref Expression
1 bnj571.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
2 bnj571.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
3 bnj571.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
4 bnj571.18 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
5 bnj571.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
6 bnj571.20 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
7 bnj571.22 ⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
8 bnj571.23 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
9 bnj571.24 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
10 bnj571.25 ⊢ 𝐿 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
11 bnj571.26 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
12 bnj571.29 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13 bnj571.30 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
14 bnj571.38 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 )
15 bnj571.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
16 bnj571.40 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
17 bnj571.33 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
18 nfv ⊢ Ⅎ 𝑖 𝑅 FrSe 𝐴
19 nfv ⊢ Ⅎ 𝑖 𝑓 Fn 𝑚
20 nfv ⊢ Ⅎ 𝑖 𝜑′
21 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
22 13 21 nfxfr ⊢ Ⅎ 𝑖 𝜓′
23 19 20 22 nf3an ⊢ Ⅎ 𝑖 ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ )
24 3 23 nfxfr ⊢ Ⅎ 𝑖 𝜏
25 nfv ⊢ Ⅎ 𝑖 𝜂
26 18 24 25 nf3an ⊢ Ⅎ 𝑖 ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 )
27 df-bnj17 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) )
28 3anass ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) ) )
29 3anrot ⊢ ( ( 𝑚 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) )
30 df-3an ⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) )
31 6 30 bitri ⊢ ( 𝜁 ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) )
32 31 anbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 = suc 𝑖 ) ) )
33 28 29 32 3bitr4ri ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜁 ) ↔ ( 𝑚 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) )
34 27 33 bitri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) ↔ ( 𝑚 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj558 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )
36 34 35 sylbir ⊢ ( ( 𝑚 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )
37 36 3expib ⊢ ( 𝑚 = suc 𝑖 → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )
38 df-bnj17 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜌 ) )
39 3anass ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) ) )
40 3anrot ⊢ ( ( 𝑚 ≠ suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) )
41 df-3an ⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) )
42 15 41 bitri ⊢ ( 𝜌 ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) )
43 42 anbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜌 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑚 ≠ suc 𝑖 ) ) )
44 39 40 43 3bitr4ri ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝜌 ) ↔ ( 𝑚 ≠ suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) )
45 38 44 bitri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) ↔ ( 𝑚 ≠ suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) )
46 1 3 5 15 9 2 16 13 bnj570 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )
47 45 46 sylbir ⊢ ( ( 𝑚 ≠ suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )
48 47 3expib ⊢ ( 𝑚 ≠ suc 𝑖 → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 ) )
49 37 48 pm2.61ine ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )
50 49 9 eqtrdi ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
51 50 exp32 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
52 26 51 alrimi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
53 17 bnj946 ⊢ ( 𝜓″ ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
54 52 53 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝜓″ )