Metamath Proof Explorer

Theorem bnj611

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 bnj611.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj611.2 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
bnj611.3 ⊢ 𝐺 ∈ V
Assertion bnj611 ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 bnj611.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj611.2 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
3 bnj611.3 ⊢ 𝐺 ∈ V
4 df-ral ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
5 4 bicomi ⊢ ( ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6 5 sbcbii ⊢ ( [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
7 nfv ⊢ Ⅎ 𝑓 𝑖 ∈ ω
8 7 sbc19.21g ⊢ ( 𝐺 ∈ V → ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
9 3 8 ax-mp ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
10 nfv ⊢ Ⅎ 𝑓 suc 𝑖 ∈ 𝑁
11 10 sbc19.21g ⊢ ( 𝐺 ∈ V → ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12 3 11 ax-mp ⊢ ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝐺 ‘ suc 𝑖 ) )
14 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) )
15 14 bnj1113 ⊢ ( 𝑓 = 𝐺 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
16 13 15 eqeq12d ⊢ ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
17 fveq1 ⊢ ( 𝑓 = 𝑒 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝑒 ‘ suc 𝑖 ) )
18 fveq1 ⊢ ( 𝑓 = 𝑒 → ( 𝑓 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
19 18 bnj1113 ⊢ ( 𝑓 = 𝑒 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
20 17 19 eqeq12d ⊢ ( 𝑓 = 𝑒 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑒 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
21 fveq1 ⊢ ( 𝑒 = 𝐺 → ( 𝑒 ‘ suc 𝑖 ) = ( 𝐺 ‘ suc 𝑖 ) )
22 fveq1 ⊢ ( 𝑒 = 𝐺 → ( 𝑒 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) )
23 22 bnj1113 ⊢ ( 𝑒 = 𝐺 → ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
24 21 23 eqeq12d ⊢ ( 𝑒 = 𝐺 → ( ( 𝑒 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
25 3 16 20 24 bnj610 ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
26 25 imbi2i ⊢ ( ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
27 12 26 bitri ⊢ ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
28 27 imbi2i ⊢ ( ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
29 9 28 bitri ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
30 29 albii ⊢ ( ∀ 𝑖 [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
31 sbcal ⊢ ( [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
32 df-ral ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
33 30 31 32 3bitr4ri ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
34 1 sbcbii ⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
35 6 33 34 3bitr4ri ⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
36 2 35 bitri ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )