Step |
Hyp |
Ref |
Expression |
1 |
|
frrlem5.1 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } |
2 |
|
frrlem5.2 |
⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 ) |
3 |
|
vex |
⊢ 𝑧 ∈ V |
4 |
3
|
eldm2 |
⊢ ( 𝑧 ∈ dom 𝐹 ↔ ∃ 𝑤 〈 𝑧 , 𝑤 〉 ∈ 𝐹 ) |
5 |
1 2
|
frrlem5 |
⊢ 𝐹 = ∪ 𝐵 |
6 |
1
|
frrlem1 |
⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } |
7 |
6
|
unieqi |
⊢ ∪ 𝐵 = ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } |
8 |
5 7
|
eqtri |
⊢ 𝐹 = ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } |
9 |
8
|
eleq2i |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ 𝐹 ↔ 〈 𝑧 , 𝑤 〉 ∈ ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } ) |
10 |
|
eluniab |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } ↔ ∃ 𝑔 ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) ) |
11 |
9 10
|
bitri |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ 𝐹 ↔ ∃ 𝑔 ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) ) |
12 |
|
simpr2r |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) |
13 |
|
vex |
⊢ 𝑤 ∈ V |
14 |
3 13
|
opeldm |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 → 𝑧 ∈ dom 𝑔 ) |
15 |
14
|
adantr |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑧 ∈ dom 𝑔 ) |
16 |
|
simpr1 |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 Fn 𝑎 ) |
17 |
16
|
fndmd |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → dom 𝑔 = 𝑎 ) |
18 |
15 17
|
eleqtrd |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑧 ∈ 𝑎 ) |
19 |
|
rsp |
⊢ ( ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 → ( 𝑧 ∈ 𝑎 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ) |
20 |
12 18 19
|
sylc |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) |
21 |
20 17
|
sseqtrrd |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝑔 ) |
22 |
|
19.8a |
⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
23 |
6
|
abeq2i |
⊢ ( 𝑔 ∈ 𝐵 ↔ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) |
24 |
22 23
|
sylibr |
⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → 𝑔 ∈ 𝐵 ) |
25 |
24
|
adantl |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ∈ 𝐵 ) |
26 |
|
elssuni |
⊢ ( 𝑔 ∈ 𝐵 → 𝑔 ⊆ ∪ 𝐵 ) |
27 |
25 26
|
syl |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ⊆ ∪ 𝐵 ) |
28 |
27 5
|
sseqtrrdi |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ⊆ 𝐹 ) |
29 |
|
dmss |
⊢ ( 𝑔 ⊆ 𝐹 → dom 𝑔 ⊆ dom 𝐹 ) |
30 |
28 29
|
syl |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → dom 𝑔 ⊆ dom 𝐹 ) |
31 |
21 30
|
sstrd |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |
32 |
31
|
expcom |
⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) ) |
33 |
32
|
exlimiv |
⊢ ( ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) ) |
34 |
33
|
impcom |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |
35 |
34
|
exlimiv |
⊢ ( ∃ 𝑔 ( 〈 𝑧 , 𝑤 〉 ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |
36 |
11 35
|
sylbi |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |
37 |
36
|
exlimiv |
⊢ ( ∃ 𝑤 〈 𝑧 , 𝑤 〉 ∈ 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |
38 |
4 37
|
sylbi |
⊢ ( 𝑧 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) |