Metamath Proof Explorer

Theorem bnj1006

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

Proof

Step Hyp Ref Expression
1 bnj1006.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1006.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1006.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4 bnj1006.4 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5 bnj1006.5 ⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
6 bnj1006.6 ⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
7 bnj1006.7 ⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
8 bnj1006.8 ⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
9 bnj1006.9 ⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
10 bnj1006.10 ⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
11 bnj1006.11 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
12 bnj1006.12 ⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
13 bnj1006.13 ⊢ 𝐷 = ( ω ∖ { ∅ } )
14 bnj1006.15 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
15 bnj1006.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
16 bnj1006.28 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )
17 6 simprbi ⊢ ( 𝜂 → 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
18 17 bnj708 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
19 bnj253 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
20 19 simp1bi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
21 4 20 sylbi ⊢ ( 𝜃 → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
22 21 bnj705 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
23 bnj643 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒 )
24 3simpc ⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
25 5 24 sylbi ⊢ ( 𝜏 → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
26 25 bnj707 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
27 3anass ⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ↔ ( 𝜒 ∧ ( 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) )
28 23 26 27 sylanbrc ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
29 biid ⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
30 biid ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) )
31 1 2 3 13 14 29 30 bnj969 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V )
32 22 28 31 syl2anc ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝐶 ∈ V )
33 3 bnj1235 ⊢ ( 𝜒 → 𝑓 Fn 𝑛 )
34 33 bnj706 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑓 Fn 𝑛 )
35 5 simp3bi ⊢ ( 𝜏 → 𝑝 = suc 𝑛 )
36 35 bnj707 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑝 = suc 𝑛 )
37 6 simplbi ⊢ ( 𝜂 → 𝑖 ∈ 𝑛 )
38 37 bnj708 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑖 ∈ 𝑛 )
39 32 34 36 38 bnj951 ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) )
40 15 bnj945 ⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
41 39 40 syl ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
42 18 41 eleqtrrd ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) )
43 16 anim1i ⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
44 df-bnj17 ⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ↔ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
45 43 44 sylibr ⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
46 1 2 3 7 8 9 10 11 12 14 15 bnj999 ⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )
47 45 46 syl ⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )
48 42 47 mpdan ⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )