Metamath Proof Explorer

Theorem bnj967

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 bnj967.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj967.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj967.10 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj967.12 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj967.13 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
bnj967.44 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
Assertion bnj967 ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj967.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj967.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
3 bnj967.10 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj967.12 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
5 bnj967.13 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
6 bnj967.44 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
7 6 3adant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → 𝐶 ∈ V )
8 2 bnj1235 ⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
9 8 3ad2ant1 ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 )
10 9 3ad2ant2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → 𝑓 Fn 𝑛 )
11 simp23 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → 𝑝 = suc 𝑛 )
12 simp3 ⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) → suc 𝑖 ∈ 𝑛 )
13 12 3ad2ant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → suc 𝑖 ∈ 𝑛 )
14 7 10 11 13 bnj951 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) )
15 3 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
16 2 15 bnj769 ⊢ ( 𝜒 → 𝑛 ∈ ω )
17 16 3ad2ant1 ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑛 ∈ ω )
18 17 12 bnj240 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝑛 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) )
19 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
20 ordtr ⊢ ( Ord 𝑛 → Tr 𝑛 )
21 19 20 syl ⊢ ( 𝑛 ∈ ω → Tr 𝑛 )
22 trsuc ⊢ ( ( Tr 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) → 𝑖 ∈ 𝑛 )
23 21 22 sylan ⊢ ( ( 𝑛 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) → 𝑖 ∈ 𝑛 )
24 18 23 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → 𝑖 ∈ 𝑛 )
25 bnj658 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) )
26 25 anim1i ⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) → ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) )
27 df-bnj17 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) ↔ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) )
28 26 27 sylibr ⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) )
29 14 24 28 syl2anc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) )
30 5 bnj945 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
31 29 30 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
32 5 bnj945 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) )
33 14 32 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) )
34 3simpb ⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) )
35 34 3ad2ant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) )
36 2 bnj1254 ⊢ ( 𝜒 → 𝜓 )
37 36 3ad2ant1 ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝜓 )
38 37 3ad2ant2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → 𝜓 )
39 31 33 35 38 bnj951 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) )
40 4 5 bnj958 ⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
41 1 40 bnj953 ⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
42 39 41 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )