Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . . . 5
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
2 | 1 | tfrlem7 7366 |
. . . 4
⊢ Fun
recs(𝐹) |
3 | | funfvop 6237 |
. . . 4
⊢ ((Fun
recs(𝐹) ∧ 𝐵 ∈ dom recs(𝐹)) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ recs(𝐹)) |
4 | 2, 3 | mpan 702 |
. . 3
⊢ (𝐵 ∈ dom recs(𝐹) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ recs(𝐹)) |
5 | 1 | recsfval 7364 |
. . . . 5
⊢
recs(𝐹) = ∪ 𝐴 |
6 | 5 | eleq2i 2680 |
. . . 4
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ recs(𝐹) ↔ 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ ∪
𝐴) |
7 | | eluni 4375 |
. . . 4
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ ∪ 𝐴
↔ ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) |
8 | 6, 7 | bitri 263 |
. . 3
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ recs(𝐹) ↔ ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) |
9 | 4, 8 | sylib 207 |
. 2
⊢ (𝐵 ∈ dom recs(𝐹) → ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) |
10 | | simprr 792 |
. . . 4
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → 𝑔 ∈ 𝐴) |
11 | | vex 3176 |
. . . . 5
⊢ 𝑔 ∈ V |
12 | 1, 11 | tfrlem3a 7360 |
. . . 4
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) |
13 | 10, 12 | sylib 207 |
. . 3
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) |
14 | 2 | a1i 11 |
. . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → Fun recs(𝐹)) |
15 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ∈ 𝐴) |
16 | | elssuni 4403 |
. . . . . . . . . 10
⊢ (𝑔 ∈ 𝐴 → 𝑔 ⊆ ∪ 𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ⊆ ∪ 𝐴) |
18 | 17, 5 | syl6sseqr 3615 |
. . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ⊆ recs(𝐹)) |
19 | | fndm 5904 |
. . . . . . . . . . . 12
⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧) |
20 | 19 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → dom 𝑔 = 𝑧) |
21 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑧 ∈ On) |
22 | 20, 21 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → dom 𝑔 ∈ On) |
23 | | eloni 5650 |
. . . . . . . . . 10
⊢ (dom
𝑔 ∈ On → Ord dom
𝑔) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → Ord dom 𝑔) |
25 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ∈ dom recs(𝐹)) |
26 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(recs(𝐹)‘𝐵) ∈ V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹)‘𝐵) ∈ V) |
28 | | simplrl 796 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔) |
29 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝐵𝑔(recs(𝐹)‘𝐵) ↔ 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔) |
30 | 28, 29 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵𝑔(recs(𝐹)‘𝐵)) |
31 | | breldmg 5252 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (recs(𝐹)‘𝐵) ∈ V ∧ 𝐵𝑔(recs(𝐹)‘𝐵)) → 𝐵 ∈ dom 𝑔) |
32 | 25, 27, 30, 31 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ∈ dom 𝑔) |
33 | | ordelss 5656 |
. . . . . . . . 9
⊢ ((Ord dom
𝑔 ∧ 𝐵 ∈ dom 𝑔) → 𝐵 ⊆ dom 𝑔) |
34 | 24, 32, 33 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ⊆ dom 𝑔) |
35 | | fun2ssres 5845 |
. . . . . . . 8
⊢ ((Fun
recs(𝐹) ∧ 𝑔 ⊆ recs(𝐹) ∧ 𝐵 ⊆ dom 𝑔) → (recs(𝐹) ↾ 𝐵) = (𝑔 ↾ 𝐵)) |
36 | 14, 18, 34, 35 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹) ↾ 𝐵) = (𝑔 ↾ 𝐵)) |
37 | 11 | resex 5363 |
. . . . . . . 8
⊢ (𝑔 ↾ 𝐵) ∈ V |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (𝑔 ↾ 𝐵) ∈ V) |
39 | 36, 38 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹) ↾ 𝐵) ∈ V) |
40 | 39 | expr 641 |
. . . . 5
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ 𝑧 ∈ On) → (𝑔 Fn 𝑧 → (recs(𝐹) ↾ 𝐵) ∈ V)) |
41 | 40 | adantrd 483 |
. . . 4
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ 𝑧 ∈ On) → ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) → (recs(𝐹) ↾ 𝐵) ∈ V)) |
42 | 41 | rexlimdva 3013 |
. . 3
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) → (recs(𝐹) ↾ 𝐵) ∈ V)) |
43 | 13, 42 | mpd 15 |
. 2
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → (recs(𝐹) ↾ 𝐵) ∈ V) |
44 | 9, 43 | exlimddv 1850 |
1
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V) |