Theorem bnj999

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

Proof

Step	Hyp	Ref	Expression
1		bnj999.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj999.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj999.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj999.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
5		bnj999.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
6		bnj999.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
7		bnj999.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
8		bnj999.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
9		bnj999.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
10		bnj999.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
11		bnj999.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
12		vex	⊢ 𝑝 ∈ V
13	3 4 5 6 12	bnj919	⊢ ( 𝜒′ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′ ) )
14	11	bnj918	⊢ 𝐺 ∈ V
15	13 7 8 9 14	bnj976	⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
16	15	bnj1254	⊢ ( 𝜒″ → 𝜓″ )
17	16	anim1i	⊢ ( ( 𝜒″ ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ) → ( 𝜓″ ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ) )
18		bnj252	⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ↔ ( 𝜒″ ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ) )
19		bnj252	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ↔ ( 𝜓″ ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) ) )
20	17 18 19	3imtr4i	⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) )
21		ssiun2	⊢ ( 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
22	21	bnj708	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
23		3simpa	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝜓″ ∧ 𝑖 ∈ ω ) )
24	23	ancomd	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝑖 ∈ ω ∧ 𝜓″ ) )
25		simp3	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → suc 𝑖 ∈ 𝑝 )
26	2 5 12	bnj539	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑝 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
27	26 8 10 11	bnj965	⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑝 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
28	27	bnj228	⊢ ( ( 𝑖 ∈ ω ∧ 𝜓″ ) → ( suc 𝑖 ∈ 𝑝 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
29	24 25 28	sylc	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
30	29	bnj721	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
31	22 30	sseqtrrd	⊢ ( ( 𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )
32	20 31	syl	⊢ ( ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( 𝐺 ‘ suc 𝑖 ) )