Step |
Hyp |
Ref |
Expression |
1 |
|
bnj964.2 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
2 |
|
bnj964.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
3 |
|
bnj964.5 |
⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 ) |
4 |
|
bnj964.8 |
⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ ) |
5 |
|
bnj964.12 |
⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
6 |
|
bnj964.13 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
7 |
|
bnj964.96 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
8 |
|
bnj964.165 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
9 |
|
nfv |
⊢ Ⅎ 𝑖 ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) |
10 |
1
|
bnj1095 |
⊢ ( 𝜓 → ∀ 𝑖 𝜓 ) |
11 |
10 2
|
bnj1096 |
⊢ ( 𝜒 → ∀ 𝑖 𝜒 ) |
12 |
11
|
nf5i |
⊢ Ⅎ 𝑖 𝜒 |
13 |
|
nfv |
⊢ Ⅎ 𝑖 𝑛 = suc 𝑚 |
14 |
|
nfv |
⊢ Ⅎ 𝑖 𝑝 = suc 𝑛 |
15 |
12 13 14
|
nf3an |
⊢ Ⅎ 𝑖 ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) |
16 |
9 15
|
nfan |
⊢ Ⅎ 𝑖 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) |
17 |
|
bnj255 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) |
18 |
|
bnj645 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → suc 𝑖 ∈ 𝑝 ) |
19 |
|
simp3 |
⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑝 = suc 𝑛 ) |
20 |
19
|
bnj706 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → 𝑝 = suc 𝑛 ) |
21 |
|
eleq2 |
⊢ ( 𝑝 = suc 𝑛 → ( suc 𝑖 ∈ 𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) ) |
22 |
21
|
biimpac |
⊢ ( ( suc 𝑖 ∈ 𝑝 ∧ 𝑝 = suc 𝑛 ) → suc 𝑖 ∈ suc 𝑛 ) |
23 |
|
elsuci |
⊢ ( suc 𝑖 ∈ suc 𝑛 → ( suc 𝑖 ∈ 𝑛 ∨ suc 𝑖 = 𝑛 ) ) |
24 |
|
eqcom |
⊢ ( suc 𝑖 = 𝑛 ↔ 𝑛 = suc 𝑖 ) |
25 |
24
|
orbi2i |
⊢ ( ( suc 𝑖 ∈ 𝑛 ∨ suc 𝑖 = 𝑛 ) ↔ ( suc 𝑖 ∈ 𝑛 ∨ 𝑛 = suc 𝑖 ) ) |
26 |
23 25
|
sylib |
⊢ ( suc 𝑖 ∈ suc 𝑛 → ( suc 𝑖 ∈ 𝑛 ∨ 𝑛 = suc 𝑖 ) ) |
27 |
22 26
|
syl |
⊢ ( ( suc 𝑖 ∈ 𝑝 ∧ 𝑝 = suc 𝑛 ) → ( suc 𝑖 ∈ 𝑛 ∨ 𝑛 = suc 𝑖 ) ) |
28 |
18 20 27
|
syl2anc |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( suc 𝑖 ∈ 𝑛 ∨ 𝑛 = suc 𝑖 ) ) |
29 |
|
df-3an |
⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ) |
30 |
29
|
3anbi3i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ) ) |
31 |
|
bnj255 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ) ) |
32 |
30 31
|
bitr4i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ) |
33 |
|
bnj345 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ suc 𝑖 ∈ 𝑛 ) ↔ ( suc 𝑖 ∈ 𝑛 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) |
34 |
|
bnj252 |
⊢ ( ( suc 𝑖 ∈ 𝑛 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ↔ ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
35 |
32 33 34
|
3bitri |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
36 |
17
|
anbi2i |
⊢ ( ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ↔ ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
37 |
35 36
|
bitr4i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) ↔ ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) |
38 |
37 7
|
sylbir |
⊢ ( ( suc 𝑖 ∈ 𝑛 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
39 |
38
|
ex |
⊢ ( suc 𝑖 ∈ 𝑛 → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
40 |
|
df-3an |
⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ↔ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) |
41 |
40
|
3anbi3i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) ) |
42 |
|
bnj255 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) ) |
43 |
41 42
|
bitr4i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ) |
44 |
|
bnj345 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ∧ 𝑛 = suc 𝑖 ) ↔ ( 𝑛 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) |
45 |
|
bnj252 |
⊢ ( ( 𝑛 = suc 𝑖 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
46 |
43 44 45
|
3bitri |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
47 |
17
|
anbi2i |
⊢ ( ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) ) |
48 |
46 47
|
bitr4i |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) ↔ ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) ) |
49 |
48 8
|
sylbir |
⊢ ( ( 𝑛 = suc 𝑖 ∧ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
50 |
49
|
ex |
⊢ ( 𝑛 = suc 𝑖 → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
51 |
39 50
|
jaoi |
⊢ ( ( suc 𝑖 ∈ 𝑛 ∨ 𝑛 = suc 𝑖 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
52 |
28 51
|
mpcom |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
53 |
17 52
|
sylbir |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
54 |
53
|
3expia |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
55 |
16 54
|
alrimi |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
56 |
|
vex |
⊢ 𝑝 ∈ V |
57 |
1 3 56
|
bnj539 |
⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑝 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
58 |
57 4 5 6
|
bnj965 |
⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑝 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
59 |
58
|
bnj115 |
⊢ ( 𝜓″ ↔ ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
60 |
55 59
|
sylibr |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜓″ ) |