Step |
Hyp |
Ref |
Expression |
1 |
|
bnj544.1 |
⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |
2 |
|
bnj544.2 |
⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
3 |
|
bnj544.3 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
4 |
|
bnj544.4 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) 〉 } ) |
5 |
|
bnj544.5 |
⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) |
6 |
|
bnj544.6 |
⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) |
7 |
3
|
bnj923 |
⊢ ( 𝑚 ∈ 𝐷 → 𝑚 ∈ ω ) |
8 |
7
|
3anim1i |
⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) → ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) |
9 |
6 8
|
sylbi |
⊢ ( 𝜎 → ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) |
10 |
|
biid |
⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) |
11 |
1 2 4 5 10
|
bnj543 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) → 𝐺 Fn 𝑛 ) |
12 |
9 11
|
syl3an3 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 ) |