Step |
Hyp |
Ref |
Expression |
1 |
|
bnj545.1 |
⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |
2 |
|
bnj545.2 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
3 |
|
bnj545.3 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) 〉 } ) |
4 |
|
bnj545.4 |
⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) |
5 |
|
bnj545.5 |
⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ) |
6 |
|
bnj545.6 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 ) |
7 |
|
bnj545.7 |
⊢ ( 𝜑″ ↔ ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |
8 |
4
|
simp1bi |
⊢ ( 𝜏 → 𝑓 Fn 𝑚 ) |
9 |
5
|
simp1bi |
⊢ ( 𝜎 → 𝑚 ∈ 𝐷 ) |
10 |
8 9
|
anim12i |
⊢ ( ( 𝜏 ∧ 𝜎 ) → ( 𝑓 Fn 𝑚 ∧ 𝑚 ∈ 𝐷 ) ) |
11 |
10
|
3adant1 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( 𝑓 Fn 𝑚 ∧ 𝑚 ∈ 𝐷 ) ) |
12 |
2
|
bnj529 |
⊢ ( 𝑚 ∈ 𝐷 → ∅ ∈ 𝑚 ) |
13 |
|
fndm |
⊢ ( 𝑓 Fn 𝑚 → dom 𝑓 = 𝑚 ) |
14 |
|
eleq2 |
⊢ ( dom 𝑓 = 𝑚 → ( ∅ ∈ dom 𝑓 ↔ ∅ ∈ 𝑚 ) ) |
15 |
14
|
biimparc |
⊢ ( ( ∅ ∈ 𝑚 ∧ dom 𝑓 = 𝑚 ) → ∅ ∈ dom 𝑓 ) |
16 |
12 13 15
|
syl2anr |
⊢ ( ( 𝑓 Fn 𝑚 ∧ 𝑚 ∈ 𝐷 ) → ∅ ∈ dom 𝑓 ) |
17 |
11 16
|
syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ∅ ∈ dom 𝑓 ) |
18 |
6
|
bnj930 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → Fun 𝐺 ) |
19 |
17 18
|
jca |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) |
20 |
3
|
bnj931 |
⊢ 𝑓 ⊆ 𝐺 |
21 |
19 20
|
jctil |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( 𝑓 ⊆ 𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) ) |
22 |
|
df-3an |
⊢ ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ) ↔ ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ∧ 𝑓 ⊆ 𝐺 ) ) |
23 |
|
3anrot |
⊢ ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ) ↔ ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ ∅ ∈ dom 𝑓 ) ) |
24 |
|
ancom |
⊢ ( ( ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ∧ 𝑓 ⊆ 𝐺 ) ↔ ( 𝑓 ⊆ 𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) ) |
25 |
22 23 24
|
3bitr3i |
⊢ ( ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ ∅ ∈ dom 𝑓 ) ↔ ( 𝑓 ⊆ 𝐺 ∧ ( ∅ ∈ dom 𝑓 ∧ Fun 𝐺 ) ) ) |
26 |
21 25
|
sylibr |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ ∅ ∈ dom 𝑓 ) ) |
27 |
|
funssfv |
⊢ ( ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ ∅ ∈ dom 𝑓 ) → ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ) |
28 |
26 27
|
syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ) |
29 |
4
|
simp2bi |
⊢ ( 𝜏 → 𝜑′ ) |
30 |
29
|
3ad2ant2 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝜑′ ) |
31 |
|
eqtr |
⊢ ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |
32 |
1 31
|
sylan2b |
⊢ ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ 𝜑′ ) → ( 𝐺 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |
33 |
32 7
|
sylibr |
⊢ ( ( ( 𝐺 ‘ ∅ ) = ( 𝑓 ‘ ∅ ) ∧ 𝜑′ ) → 𝜑″ ) |
34 |
28 30 33
|
syl2anc |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝜑″ ) |