Theorem bnj518

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	bnj518.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj518.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj518.3	⊢ ( 𝜏 ↔ ( 𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛 ) )
Assertion	bnj518	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		bnj518.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj518.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj518.3	⊢ ( 𝜏 ↔ ( 𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛 ) )
4		bnj334	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛 ) ↔ ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛 ) )
5	3 4	bitri	⊢ ( 𝜏 ↔ ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛 ) )
6		df-bnj17	⊢ ( ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛 ) ↔ ( ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑝 ∈ 𝑛 ) )
7	1 2	bnj517	⊢ ( ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ) → ∀ 𝑝 ∈ 𝑛 ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 )
8	7	r19.21bi	⊢ ( ( ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑝 ∈ 𝑛 ) → ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 )
9	6 8	sylbi	⊢ ( ( 𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛 ) → ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 )
10	5 9	sylbi	⊢ ( 𝜏 → ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 )
11		ssel	⊢ ( ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 → ( 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) → 𝑦 ∈ 𝐴 ) )
12		bnj93	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
13	12	ex	⊢ ( 𝑅 FrSe 𝐴 → ( 𝑦 ∈ 𝐴 → pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) )
14	11 13	sylan9r	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) )
15	14	ralrimiv	⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝑓 ‘ 𝑝 ) ⊆ 𝐴 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
16	10 15	sylan2	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )