| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tfrlem.1 | . . . . 5
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | 
| 2 | 1 | tfrlem7 8423 | . . . 4
⊢ Fun
recs(𝐹) | 
| 3 |  | funfvop 7070 | . . . 4
⊢ ((Fun
recs(𝐹) ∧ 𝐵 ∈ dom recs(𝐹)) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ recs(𝐹)) | 
| 4 | 2, 3 | mpan 690 | . . 3
⊢ (𝐵 ∈ dom recs(𝐹) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ recs(𝐹)) | 
| 5 | 1 | recsfval 8421 | . . . . 5
⊢
recs(𝐹) = ∪ 𝐴 | 
| 6 | 5 | eleq2i 2833 | . . . 4
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ recs(𝐹) ↔ 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ ∪
𝐴) | 
| 7 |  | eluni 4910 | . . . 4
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ ∪ 𝐴
↔ ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) | 
| 8 | 6, 7 | bitri 275 | . . 3
⊢
(〈𝐵,
(recs(𝐹)‘𝐵)〉 ∈ recs(𝐹) ↔ ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) | 
| 9 | 4, 8 | sylib 218 | . 2
⊢ (𝐵 ∈ dom recs(𝐹) → ∃𝑔(〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) | 
| 10 |  | simprr 773 | . . . 4
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → 𝑔 ∈ 𝐴) | 
| 11 |  | vex 3484 | . . . . 5
⊢ 𝑔 ∈ V | 
| 12 | 1, 11 | tfrlem3a 8417 | . . . 4
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) | 
| 13 | 10, 12 | sylib 218 | . . 3
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) | 
| 14 | 2 | a1i 11 | . . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → Fun recs(𝐹)) | 
| 15 |  | simplrr 778 | . . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ∈ 𝐴) | 
| 16 |  | elssuni 4937 | . . . . . . . . . 10
⊢ (𝑔 ∈ 𝐴 → 𝑔 ⊆ ∪ 𝐴) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ⊆ ∪ 𝐴) | 
| 18 | 17, 5 | sseqtrrdi 4025 | . . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑔 ⊆ recs(𝐹)) | 
| 19 |  | fndm 6671 | . . . . . . . . . . . 12
⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧) | 
| 20 | 19 | ad2antll 729 | . . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → dom 𝑔 = 𝑧) | 
| 21 |  | simprl 771 | . . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝑧 ∈ On) | 
| 22 | 20, 21 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → dom 𝑔 ∈ On) | 
| 23 |  | eloni 6394 | . . . . . . . . . 10
⊢ (dom
𝑔 ∈ On → Ord dom
𝑔) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → Ord dom 𝑔) | 
| 25 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ∈ dom recs(𝐹)) | 
| 26 |  | fvexd 6921 | . . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹)‘𝐵) ∈ V) | 
| 27 |  | simplrl 777 | . . . . . . . . . . 11
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔) | 
| 28 |  | df-br 5144 | . . . . . . . . . . 11
⊢ (𝐵𝑔(recs(𝐹)‘𝐵) ↔ 〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔) | 
| 29 | 27, 28 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵𝑔(recs(𝐹)‘𝐵)) | 
| 30 |  | breldmg 5920 | . . . . . . . . . 10
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (recs(𝐹)‘𝐵) ∈ V ∧ 𝐵𝑔(recs(𝐹)‘𝐵)) → 𝐵 ∈ dom 𝑔) | 
| 31 | 25, 26, 29, 30 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ∈ dom 𝑔) | 
| 32 |  | ordelss 6400 | . . . . . . . . 9
⊢ ((Ord dom
𝑔 ∧ 𝐵 ∈ dom 𝑔) → 𝐵 ⊆ dom 𝑔) | 
| 33 | 24, 31, 32 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → 𝐵 ⊆ dom 𝑔) | 
| 34 |  | fun2ssres 6611 | . . . . . . . 8
⊢ ((Fun
recs(𝐹) ∧ 𝑔 ⊆ recs(𝐹) ∧ 𝐵 ⊆ dom 𝑔) → (recs(𝐹) ↾ 𝐵) = (𝑔 ↾ 𝐵)) | 
| 35 | 14, 18, 33, 34 | syl3anc 1373 | . . . . . . 7
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹) ↾ 𝐵) = (𝑔 ↾ 𝐵)) | 
| 36 | 11 | resex 6047 | . . . . . . . 8
⊢ (𝑔 ↾ 𝐵) ∈ V | 
| 37 | 36 | a1i 11 | . . . . . . 7
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (𝑔 ↾ 𝐵) ∈ V) | 
| 38 | 35, 37 | eqeltrd 2841 | . . . . . 6
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ (𝑧 ∈ On ∧ 𝑔 Fn 𝑧)) → (recs(𝐹) ↾ 𝐵) ∈ V) | 
| 39 | 38 | expr 456 | . . . . 5
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ 𝑧 ∈ On) → (𝑔 Fn 𝑧 → (recs(𝐹) ↾ 𝐵) ∈ V)) | 
| 40 | 39 | adantrd 491 | . . . 4
⊢ (((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) ∧ 𝑧 ∈ On) → ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) → (recs(𝐹) ↾ 𝐵) ∈ V)) | 
| 41 | 40 | rexlimdva 3155 | . . 3
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) → (recs(𝐹) ↾ 𝐵) ∈ V)) | 
| 42 | 13, 41 | mpd 15 | . 2
⊢ ((𝐵 ∈ dom recs(𝐹) ∧ (〈𝐵, (recs(𝐹)‘𝐵)〉 ∈ 𝑔 ∧ 𝑔 ∈ 𝐴)) → (recs(𝐹) ↾ 𝐵) ∈ V) | 
| 43 | 9, 42 | exlimddv 1935 | 1
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V) |