| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dnnumch.a | . 2
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 2 |  | recsval 8444 | . . . . . . 7
⊢ (𝑥 ∈ On → (recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))‘𝑥) = ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) ↾ 𝑥))) | 
| 3 |  | dnnumch.f | . . . . . . . 8
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) | 
| 4 | 3 | fveq1i 6907 | . . . . . . 7
⊢ (𝐹‘𝑥) = (recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))‘𝑥) | 
| 5 | 3 | tfr1 8437 | . . . . . . . . . . 11
⊢ 𝐹 Fn On | 
| 6 |  | fnfun 6668 | . . . . . . . . . . 11
⊢ (𝐹 Fn On → Fun 𝐹) | 
| 7 | 5, 6 | ax-mp 5 | . . . . . . . . . 10
⊢ Fun 𝐹 | 
| 8 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑥 ∈ V | 
| 9 |  | resfunexg 7235 | . . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ V) → (𝐹 ↾ 𝑥) ∈ V) | 
| 10 | 7, 8, 9 | mp2an 692 | . . . . . . . . 9
⊢ (𝐹 ↾ 𝑥) ∈ V | 
| 11 |  | rneq 5947 | . . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹 ↾ 𝑥) → ran 𝑤 = ran (𝐹 ↾ 𝑥)) | 
| 12 |  | df-ima 5698 | . . . . . . . . . . . . 13
⊢ (𝐹 “ 𝑥) = ran (𝐹 ↾ 𝑥) | 
| 13 | 11, 12 | eqtr4di 2795 | . . . . . . . . . . . 12
⊢ (𝑤 = (𝐹 ↾ 𝑥) → ran 𝑤 = (𝐹 “ 𝑥)) | 
| 14 | 13 | difeq2d 4126 | . . . . . . . . . . 11
⊢ (𝑤 = (𝐹 ↾ 𝑥) → (𝐴 ∖ ran 𝑤) = (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 15 | 14 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑤 = (𝐹 ↾ 𝑥) → (𝐺‘(𝐴 ∖ ran 𝑤)) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 16 |  | rneq 5947 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → ran 𝑧 = ran 𝑤) | 
| 17 | 16 | difeq2d 4126 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝐴 ∖ ran 𝑧) = (𝐴 ∖ ran 𝑤)) | 
| 18 | 17 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → (𝐺‘(𝐴 ∖ ran 𝑧)) = (𝐺‘(𝐴 ∖ ran 𝑤))) | 
| 19 | 18 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))) = (𝑤 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑤))) | 
| 20 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ V | 
| 21 | 15, 19, 20 | fvmpt 7016 | . . . . . . . . 9
⊢ ((𝐹 ↾ 𝑥) ∈ V → ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(𝐹 ↾ 𝑥)) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 22 | 10, 21 | ax-mp 5 | . . . . . . . 8
⊢ ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(𝐹 ↾ 𝑥)) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) | 
| 23 | 3 | reseq1i 5993 | . . . . . . . . 9
⊢ (𝐹 ↾ 𝑥) = (recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) ↾ 𝑥) | 
| 24 | 23 | fveq2i 6909 | . . . . . . . 8
⊢ ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(𝐹 ↾ 𝑥)) = ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) ↾ 𝑥)) | 
| 25 | 22, 24 | eqtr3i 2767 | . . . . . . 7
⊢ (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) = ((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))‘(recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) ↾ 𝑥)) | 
| 26 | 2, 4, 25 | 3eqtr4g 2802 | . . . . . 6
⊢ (𝑥 ∈ On → (𝐹‘𝑥) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 27 | 26 | ad2antlr 727 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅) → (𝐹‘𝑥) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 28 |  | difss 4136 | . . . . . . . . 9
⊢ (𝐴 ∖ (𝐹 “ 𝑥)) ⊆ 𝐴 | 
| 29 |  | elpw2g 5333 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ (𝐹 “ 𝑥)) ⊆ 𝐴)) | 
| 30 | 1, 29 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ (𝐹 “ 𝑥)) ⊆ 𝐴)) | 
| 31 | 28, 30 | mpbiri 258 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴) | 
| 32 |  | dnnumch.g | . . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) | 
| 33 |  | neeq1 3003 | . . . . . . . . . 10
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → (𝑦 ≠ ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅)) | 
| 34 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → (𝐺‘𝑦) = (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 35 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → 𝑦 = (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 36 | 34, 35 | eleq12d 2835 | . . . . . . . . . 10
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → ((𝐺‘𝑦) ∈ 𝑦 ↔ (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 37 | 33, 36 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → ((𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦) ↔ ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 38 | 37 | rspcva 3620 | . . . . . . . 8
⊢ (((𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 39 | 31, 32, 38 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 40 | 39 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ On) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 41 | 40 | imp 406 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅) → (𝐺‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 42 | 27, 41 | eqeltrd 2841 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅) → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 43 | 42 | ex 412 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ On) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 44 | 43 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 45 | 5 | tz7.49c 8486 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | 
| 46 | 1, 44, 45 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) |