Step |
Hyp |
Ref |
Expression |
1 |
|
bnj229.1 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
2 |
|
bnj213 |
⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 |
3 |
2
|
bnj226 |
⊢ ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 |
4 |
1
|
bnj222 |
⊢ ( 𝜓 ↔ ∀ 𝑚 ∈ ω ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
5 |
4
|
bnj228 |
⊢ ( ( 𝑚 ∈ ω ∧ 𝜓 ) → ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
7 |
|
eleq1 |
⊢ ( suc 𝑚 = 𝑛 → ( suc 𝑚 ∈ 𝑁 ↔ 𝑛 ∈ 𝑁 ) ) |
8 |
|
fveqeq2 |
⊢ ( suc 𝑚 = 𝑛 → ( ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
9 |
7 8
|
imbi12d |
⊢ ( suc 𝑚 = 𝑛 → ( ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
10 |
9
|
adantr |
⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( ( suc 𝑚 ∈ 𝑁 → ( 𝐹 ‘ suc 𝑚 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
11 |
6 10
|
mpbid |
⊢ ( ( suc 𝑚 = 𝑛 ∧ ( 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
12 |
11
|
3impb |
⊢ ( ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) → ( 𝑛 ∈ 𝑁 → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
13 |
12
|
impcom |
⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹 ‘ 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
14 |
3 13
|
bnj1262 |
⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ 𝐴 ) |