Step |
Hyp |
Ref |
Expression |
1 |
|
fprr.1 |
⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 ) |
2 |
|
eqid |
⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
3 |
2
|
frrlem1 |
⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } |
4 |
3 1
|
fprlem1 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ∧ ℎ ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑏 𝑔 𝑢 ∧ 𝑏 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) |
5 |
3 1 4
|
frrlem9 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 ) |
6 |
|
eqid |
⊢ ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ { 〈 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) 〉 } ) |
7 |
|
simp1 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 ) |
8 |
|
ssidd |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
9 |
|
fprlem2 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
10 |
|
setlikespec |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
11 |
10
|
ancoms |
⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
12 |
11
|
3ad2antl3 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
13 |
|
predss |
⊢ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 |
14 |
13
|
a1i |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 ) |
15 |
|
difssd |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ) |
16 |
|
simpr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) |
17 |
15 16
|
jca |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) ) |
18 |
|
frpomin2 |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
19 |
17 18
|
syldan |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) |
20 |
3 1 4 6 7 8 9 12 14 19
|
frrlem14 |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 ) |
21 |
|
df-fn |
⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) |
22 |
5 20 21
|
sylanbrc |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 ) |