Metamath Proof Explorer

Theorem bnj1000

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 bnj1000.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1000.2 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
bnj1000.3 ⊢ 𝐺 ∈ V
bnj1000.15 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj1000.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
Assertion bnj1000 ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 bnj1000.1 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj1000.2 ⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
3 bnj1000.3 ⊢ 𝐺 ∈ V
4 bnj1000.15 ⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
5 bnj1000.16 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
6 df-ral ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
7 6 bicomi ⊢ ( ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
8 7 sbcbii ⊢ ( [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
9 nfv ⊢ Ⅎ 𝑓 𝑖 ∈ ω
10 9 sbc19.21g ⊢ ( 𝐺 ∈ V → ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
11 3 10 ax-mp ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12 nfv ⊢ Ⅎ 𝑓 suc 𝑖 ∈ 𝑁
13 12 sbc19.21g ⊢ ( 𝐺 ∈ V → ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
14 3 13 ax-mp ⊢ ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
15 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝐺 ‘ suc 𝑖 ) )
16 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) )
17 ax-5 ⊢ ( 𝑤 ∈ ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 𝑤 ∈ ( 𝑓 ‘ 𝑖 ) )
18 nfcv ⊢ Ⅎ 𝑦 𝑓
19 nfcv ⊢ Ⅎ 𝑦 𝑛
20 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
21 4 20 nfcxfr ⊢ Ⅎ 𝑦 𝐶
22 19 21 nfop ⊢ Ⅎ 𝑦 ⟨ 𝑛 , 𝐶 ⟩
23 22 nfsn ⊢ Ⅎ 𝑦 { ⟨ 𝑛 , 𝐶 ⟩ }
24 18 23 nfun ⊢ Ⅎ 𝑦 ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
25 5 24 nfcxfr ⊢ Ⅎ 𝑦 𝐺
26 nfcv ⊢ Ⅎ 𝑦 𝑖
27 25 26 nffv ⊢ Ⅎ 𝑦 ( 𝐺 ‘ 𝑖 )
28 27 nfcrii ⊢ ( 𝑤 ∈ ( 𝐺 ‘ 𝑖 ) → ∀ 𝑦 𝑤 ∈ ( 𝐺 ‘ 𝑖 ) )
29 17 28 bnj1316 ⊢ ( ( 𝑓 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
30 16 29 syl ⊢ ( 𝑓 = 𝐺 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
31 15 30 eqeq12d ⊢ ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
32 fveq1 ⊢ ( 𝑓 = 𝑒 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝑒 ‘ suc 𝑖 ) )
33 fveq1 ⊢ ( 𝑓 = 𝑒 → ( 𝑓 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
34 ax-5 ⊢ ( ( 𝑓 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) → ∀ 𝑦 ( 𝑓 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
35 34 bnj956 ⊢ ( ( 𝑓 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
36 33 35 syl ⊢ ( 𝑓 = 𝑒 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
37 32 36 eqeq12d ⊢ ( 𝑓 = 𝑒 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑒 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
38 fveq1 ⊢ ( 𝑒 = 𝐺 → ( 𝑒 ‘ suc 𝑖 ) = ( 𝐺 ‘ suc 𝑖 ) )
39 fveq1 ⊢ ( 𝑒 = 𝐺 → ( 𝑒 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) )
40 ax-5 ⊢ ( 𝑤 ∈ ( 𝑒 ‘ 𝑖 ) → ∀ 𝑦 𝑤 ∈ ( 𝑒 ‘ 𝑖 ) )
41 40 28 bnj1316 ⊢ ( ( 𝑒 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
42 39 41 syl ⊢ ( 𝑒 = 𝐺 → ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
43 38 42 eqeq12d ⊢ ( 𝑒 = 𝐺 → ( ( 𝑒 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑒 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
44 3 31 37 43 bnj610 ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
45 44 imbi2i ⊢ ( ( suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
46 14 45 bitri ⊢ ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
47 46 imbi2i ⊢ ( ( 𝑖 ∈ ω → [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
48 11 47 bitri ⊢ ( [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
49 48 albii ⊢ ( ∀ 𝑖 [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
50 sbcal ⊢ ( [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑖 [ 𝐺 / 𝑓 ] ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
51 df-ral ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
52 49 50 51 3bitr4ri ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
53 1 sbcbii ⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
54 8 52 53 3bitr4ri ⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
55 2 54 bitri ⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )