Metamath Proof Explorer

Theorem bnj966

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

Proof

Step Hyp Ref Expression
1 bnj966.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2 bnj966.10 ⊢ 𝐷 = ( ω ∖ { ∅ } )
3 bnj966.12 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
4 bnj966.13 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
5 bnj966.44 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
6 bnj966.53 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐺 Fn 𝑝 )
7 6 bnj930 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → Fun 𝐺 )
8 7 3adant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → Fun 𝐺 )
9 opex ⊢ ⟨ 𝑛 , 𝐶 ⟩ ∈ V
10 9 snid ⊢ ⟨ 𝑛 , 𝐶 ⟩ ∈ { ⟨ 𝑛 , 𝐶 ⟩ }
11 elun2 ⊢ ( ⟨ 𝑛 , 𝐶 ⟩ ∈ { ⟨ 𝑛 , 𝐶 ⟩ } → ⟨ 𝑛 , 𝐶 ⟩ ∈ ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) )
12 10 11 ax-mp ⊢ ⟨ 𝑛 , 𝐶 ⟩ ∈ ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
13 12 4 eleqtrri ⊢ ⟨ 𝑛 , 𝐶 ⟩ ∈ 𝐺
14 funopfv ⊢ ( Fun 𝐺 → ( ⟨ 𝑛 , 𝐶 ⟩ ∈ 𝐺 → ( 𝐺 ‘ 𝑛 ) = 𝐶 ) )
15 8 13 14 mpisyl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ 𝑛 ) = 𝐶 )
16 simp22 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑛 = suc 𝑚 )
17 simp33 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑛 = suc 𝑖 )
18 bnj551 ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑛 = suc 𝑖 ) → 𝑚 = 𝑖 )
19 16 17 18 syl2anc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑚 = 𝑖 )
20 suceq ⊢ ( 𝑚 = 𝑖 → suc 𝑚 = suc 𝑖 )
21 20 eqeq2d ⊢ ( 𝑚 = 𝑖 → ( 𝑛 = suc 𝑚 ↔ 𝑛 = suc 𝑖 ) )
22 21 biimpac ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → 𝑛 = suc 𝑖 )
23 22 fveq2d ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ suc 𝑖 ) )
24 fveq2 ⊢ ( 𝑚 = 𝑖 → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑖 ) )
25 24 bnj1113 ⊢ ( 𝑚 = 𝑖 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
26 3 25 syl5eq ⊢ ( 𝑚 = 𝑖 → 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
27 26 adantl ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
28 23 27 eqeq12d ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → ( ( 𝐺 ‘ 𝑛 ) = 𝐶 ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
29 16 19 28 syl2anc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( ( 𝐺 ‘ 𝑛 ) = 𝐶 ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
30 15 29 mpbid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
31 5 3adant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝐶 ∈ V )
32 1 bnj1235 ⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
33 32 3ad2ant1 ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 )
34 33 3ad2ant2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑓 Fn 𝑛 )
35 simp23 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑝 = suc 𝑛 )
36 31 34 35 17 bnj951 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) )
37 2 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
38 1 37 bnj769 ⊢ ( 𝜒 → 𝑛 ∈ ω )
39 38 3ad2ant1 ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑛 ∈ ω )
40 simp3 ⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) → 𝑛 = suc 𝑖 )
41 39 40 bnj240 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝑛 ∈ ω ∧ 𝑛 = suc 𝑖 ) )
42 vex ⊢ 𝑖 ∈ V
43 42 bnj216 ⊢ ( 𝑛 = suc 𝑖 → 𝑖 ∈ 𝑛 )
44 43 adantl ⊢ ( ( 𝑛 ∈ ω ∧ 𝑛 = suc 𝑖 ) → 𝑖 ∈ 𝑛 )
45 41 44 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑖 ∈ 𝑛 )
46 bnj658 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) )
47 46 anim1i ⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) )
48 df-bnj17 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) ↔ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) )
49 47 48 sylibr ⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) )
50 4 bnj945 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
51 49 50 syl ⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
52 36 45 51 syl2anc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
53 3 4 bnj958 ⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
54 53 bnj956 ⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
55 54 eqeq2d ⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ( ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
56 52 55 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
57 30 56 mpbird ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )