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

Metamath Proof Explorer

Theorem bnj106

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj106.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj106.2 ⊢ 𝐹 ∈ V
Assertion bnj106 ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 bnj106.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj106.2 ⊢ 𝐹 ∈ V
3 bnj105 ⊢ 1o ∈ V
4 1 3 bnj92 ⊢ ( [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5 4 sbcbii ⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ [ 𝐹 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝐹 ‘ suc 𝑖 ) )
7 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
8 7 bnj1113 ⊢ ( 𝑓 = 𝐹 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
9 6 8 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
10 9 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
11 10 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12 2 11 sbcie ⊢ ( [ 𝐹 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13 5 12 bitri ⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )