Step |
Hyp |
Ref |
Expression |
1 |
|
bnj966.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
2 |
|
bnj966.10 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
3 |
|
bnj966.12 |
⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
4 |
|
bnj966.13 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
5 |
|
bnj966.44 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐶 ∈ V ) |
6 |
|
bnj966.53 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝐺 Fn 𝑝 ) |
7 |
6
|
bnj930 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → Fun 𝐺 ) |
8 |
7
|
3adant3 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → Fun 𝐺 ) |
9 |
|
opex |
⊢ 〈 𝑛 , 𝐶 〉 ∈ V |
10 |
9
|
snid |
⊢ 〈 𝑛 , 𝐶 〉 ∈ { 〈 𝑛 , 𝐶 〉 } |
11 |
|
elun2 |
⊢ ( 〈 𝑛 , 𝐶 〉 ∈ { 〈 𝑛 , 𝐶 〉 } → 〈 𝑛 , 𝐶 〉 ∈ ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) ) |
12 |
10 11
|
ax-mp |
⊢ 〈 𝑛 , 𝐶 〉 ∈ ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
13 |
12 4
|
eleqtrri |
⊢ 〈 𝑛 , 𝐶 〉 ∈ 𝐺 |
14 |
|
funopfv |
⊢ ( Fun 𝐺 → ( 〈 𝑛 , 𝐶 〉 ∈ 𝐺 → ( 𝐺 ‘ 𝑛 ) = 𝐶 ) ) |
15 |
8 13 14
|
mpisyl |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ 𝑛 ) = 𝐶 ) |
16 |
|
simp22 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑛 = suc 𝑚 ) |
17 |
|
simp33 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑛 = suc 𝑖 ) |
18 |
|
bnj551 |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑛 = suc 𝑖 ) → 𝑚 = 𝑖 ) |
19 |
16 17 18
|
syl2anc |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑚 = 𝑖 ) |
20 |
|
suceq |
⊢ ( 𝑚 = 𝑖 → suc 𝑚 = suc 𝑖 ) |
21 |
20
|
eqeq2d |
⊢ ( 𝑚 = 𝑖 → ( 𝑛 = suc 𝑚 ↔ 𝑛 = suc 𝑖 ) ) |
22 |
21
|
biimpac |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → 𝑛 = suc 𝑖 ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ suc 𝑖 ) ) |
24 |
|
fveq2 |
⊢ ( 𝑚 = 𝑖 → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑖 ) ) |
25 |
24
|
bnj1113 |
⊢ ( 𝑚 = 𝑖 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
26 |
3 25
|
syl5eq |
⊢ ( 𝑚 = 𝑖 → 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
27 |
26
|
adantl |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
28 |
23 27
|
eqeq12d |
⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 = 𝑖 ) → ( ( 𝐺 ‘ 𝑛 ) = 𝐶 ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
29 |
16 19 28
|
syl2anc |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( ( 𝐺 ‘ 𝑛 ) = 𝐶 ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
30 |
15 29
|
mpbid |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
31 |
5
|
3adant3 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝐶 ∈ V ) |
32 |
1
|
bnj1235 |
⊢ ( 𝜒 → 𝑓 Fn 𝑛 ) |
33 |
32
|
3ad2ant1 |
⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑓 Fn 𝑛 ) |
34 |
33
|
3ad2ant2 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑓 Fn 𝑛 ) |
35 |
|
simp23 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑝 = suc 𝑛 ) |
36 |
31 34 35 17
|
bnj951 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ) |
37 |
2
|
bnj923 |
⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω ) |
38 |
1 37
|
bnj769 |
⊢ ( 𝜒 → 𝑛 ∈ ω ) |
39 |
38
|
3ad2ant1 |
⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑛 ∈ ω ) |
40 |
|
simp3 |
⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) → 𝑛 = suc 𝑖 ) |
41 |
39 40
|
bnj240 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝑛 ∈ ω ∧ 𝑛 = suc 𝑖 ) ) |
42 |
|
vex |
⊢ 𝑖 ∈ V |
43 |
42
|
bnj216 |
⊢ ( 𝑛 = suc 𝑖 → 𝑖 ∈ 𝑛 ) |
44 |
43
|
adantl |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑛 = suc 𝑖 ) → 𝑖 ∈ 𝑛 ) |
45 |
41 44
|
syl |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → 𝑖 ∈ 𝑛 ) |
46 |
|
bnj658 |
⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ) |
47 |
46
|
anim1i |
⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) ) |
48 |
|
df-bnj17 |
⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) ↔ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ) ∧ 𝑖 ∈ 𝑛 ) ) |
49 |
47 48
|
sylibr |
⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) ) |
50 |
4
|
bnj945 |
⊢ ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
51 |
49 50
|
syl |
⊢ ( ( ( 𝐶 ∈ V ∧ 𝑓 Fn 𝑛 ∧ 𝑝 = suc 𝑛 ∧ 𝑛 = suc 𝑖 ) ∧ 𝑖 ∈ 𝑛 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
52 |
36 45 51
|
syl2anc |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
53 |
3 4
|
bnj958 |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
54 |
53
|
bnj956 |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
55 |
54
|
eqeq2d |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ( ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
56 |
52 55
|
syl |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
57 |
30 56
|
mpbird |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |