Step |
Hyp |
Ref |
Expression |
1 |
|
bnj910.1 |
⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) |
2 |
|
bnj910.2 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
3 |
|
bnj910.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
4 |
|
bnj910.4 |
⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 ) |
5 |
|
bnj910.5 |
⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 ) |
6 |
|
bnj910.6 |
⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 ) |
7 |
|
bnj910.7 |
⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ ) |
8 |
|
bnj910.8 |
⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ ) |
9 |
|
bnj910.9 |
⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ ) |
10 |
|
bnj910.10 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
11 |
|
bnj910.11 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } |
12 |
|
bnj910.12 |
⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
13 |
|
bnj910.13 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
14 |
|
bnj910.14 |
⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
15 |
|
bnj910.15 |
⊢ ( 𝜎 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛 ) ) |
16 |
3 10
|
bnj970 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 ∈ 𝐷 ) |
17 |
1 2 3 10 12 14 15
|
bnj969 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V ) |
18 |
|
simpr3 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 = suc 𝑛 ) |
19 |
3
|
bnj1235 |
⊢ ( 𝜒 → 𝑓 Fn 𝑛 ) |
20 |
19
|
3ad2ant1 |
⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 ) |
21 |
20
|
adantl |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑓 Fn 𝑛 ) |
22 |
13
|
bnj941 |
⊢ ( 𝐶 ∈ V → ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) ) |
23 |
22
|
3impib |
⊢ ( ( 𝐶 ∈ V ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) |
24 |
17 18 21 23
|
syl3anc |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐺 Fn 𝑝 ) |
25 |
1 2 3 4 7 10 12 13 14 15
|
bnj944 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜑″ ) |
26 |
2 3 10 12 13 17
|
bnj967 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
27 |
3 10 12 13 17 24
|
bnj966 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
28 |
2 3 5 8 12 13 26 27
|
bnj964 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜓″ ) |
29 |
16 24 25 28
|
bnj951 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) ) |
30 |
|
vex |
⊢ 𝑝 ∈ V |
31 |
3 4 5 6 30
|
bnj919 |
⊢ ( 𝜒′ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′ ) ) |
32 |
13
|
bnj918 |
⊢ 𝐺 ∈ V |
33 |
31 7 8 9 32
|
bnj976 |
⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) ) |
34 |
29 33
|
sylibr |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝜒″ ) |