This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )