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

Metamath Proof Explorer

Theorem bnj125

Description: Technical lemma for bnj150 . 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 bnj125.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj125.2 ⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
bnj125.3 ⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
bnj125.4 ⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
Assertion bnj125 ( 𝜑″ ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj125.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj125.2 ⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
3 bnj125.3 ⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
4 bnj125.4 ⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
5 2 sbcbii ⊢ ( [ 𝐹 / 𝑓 ] 𝜑′ ↔ [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 )
6 bnj105 ⊢ 1o ∈ V
7 1 6 bnj91 ⊢ ( [ 1o / 𝑛 ] 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
8 7 sbcbii ⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ [ 𝐹 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
9 4 bnj95 ⊢ 𝐹 ∈ V
10 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ∅ ) = ( 𝐹 ‘ ∅ ) )
11 10 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
12 9 11 sbcie ⊢ ( [ 𝐹 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13 8 12 bitri ⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
14 5 13 bitri ⊢ ( [ 𝐹 / 𝑓 ] 𝜑′ ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
15 3 14 bitri ⊢ ( 𝜑″ ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )