| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3501 | . . 3
⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | 
| 2 |  | difss 4136 | . . . . . . . . . . . 12
⊢ (𝐴 ∖ (𝐹 “ 𝑥)) ⊆ 𝐴 | 
| 3 |  | elpw2g 5333 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ V → ((𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ (𝐹 “ 𝑥)) ⊆ 𝐴)) | 
| 4 | 2, 3 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴) | 
| 5 |  | neeq1 3003 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → (𝑦 ≠ ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅)) | 
| 6 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → (𝑔‘𝑦) = (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 7 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → 𝑦 = (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 8 | 6, 7 | eleq12d 2835 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 9 | 5, 8 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝐴 ∖ (𝐹 “ 𝑥)) → ((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ↔ ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 10 | 9 | rspcv 3618 | . . . . . . . . . . 11
⊢ ((𝐴 ∖ (𝐹 “ 𝑥)) ∈ 𝒫 𝐴 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 11 | 4, 10 | syl 17 | . . . . . . . . . 10
⊢ (𝐴 ∈ V → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 12 | 11 | 3imp 1111 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅) → (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 13 |  | dfac8alem.2 | . . . . . . . . . . . 12
⊢ 𝐹 = recs(𝐺) | 
| 14 | 13 | tfr2 8438 | . . . . . . . . . . 11
⊢ (𝑥 ∈ On → (𝐹‘𝑥) = (𝐺‘(𝐹 ↾ 𝑥))) | 
| 15 | 13 | tfr1 8437 | . . . . . . . . . . . . . 14
⊢ 𝐹 Fn On | 
| 16 |  | fnfun 6668 | . . . . . . . . . . . . . 14
⊢ (𝐹 Fn On → Fun 𝐹) | 
| 17 | 15, 16 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ Fun 𝐹 | 
| 18 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 19 |  | resfunexg 7235 | . . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ V) → (𝐹 ↾ 𝑥) ∈ V) | 
| 20 | 17, 18, 19 | mp2an 692 | . . . . . . . . . . . 12
⊢ (𝐹 ↾ 𝑥) ∈ V | 
| 21 |  | rneq 5947 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐹 ↾ 𝑥) → ran 𝑓 = ran (𝐹 ↾ 𝑥)) | 
| 22 |  | df-ima 5698 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 “ 𝑥) = ran (𝐹 ↾ 𝑥) | 
| 23 | 21, 22 | eqtr4di 2795 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐹 ↾ 𝑥) → ran 𝑓 = (𝐹 “ 𝑥)) | 
| 24 | 23 | difeq2d 4126 | . . . . . . . . . . . . . 14
⊢ (𝑓 = (𝐹 ↾ 𝑥) → (𝐴 ∖ ran 𝑓) = (𝐴 ∖ (𝐹 “ 𝑥))) | 
| 25 | 24 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑓 = (𝐹 ↾ 𝑥) → (𝑔‘(𝐴 ∖ ran 𝑓)) = (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 26 |  | dfac8alem.3 | . . . . . . . . . . . . 13
⊢ 𝐺 = (𝑓 ∈ V ↦ (𝑔‘(𝐴 ∖ ran 𝑓))) | 
| 27 |  | fvex 6919 | . . . . . . . . . . . . 13
⊢ (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ V | 
| 28 | 25, 26, 27 | fvmpt 7016 | . . . . . . . . . . . 12
⊢ ((𝐹 ↾ 𝑥) ∈ V → (𝐺‘(𝐹 ↾ 𝑥)) = (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 29 | 20, 28 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝐺‘(𝐹 ↾ 𝑥)) = (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) | 
| 30 | 14, 29 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑥 ∈ On → (𝐹‘𝑥) = (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 31 | 30 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑥 ∈ On → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) ↔ (𝑔‘(𝐴 ∖ (𝐹 “ 𝑥))) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 32 | 12, 31 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝐴 ∈ V ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅) → (𝑥 ∈ On → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 33 | 32 | 3expia 1122 | . . . . . . 7
⊢ ((𝐴 ∈ V ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝑥 ∈ On → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 34 | 33 | com23 86 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → (𝑥 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 35 | 34 | ralrimiv 3145 | . . . . 5
⊢ ((𝐴 ∈ V ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) | 
| 36 | 35 | ex 412 | . . . 4
⊢ (𝐴 ∈ V → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))) | 
| 37 | 15 | tz7.49c 8486 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | 
| 38 | 37 | ex 412 | . . . . 5
⊢ (𝐴 ∈ V → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴)) | 
| 39 | 18 | f1oen 9013 | . . . . . . 7
⊢ ((𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴 → 𝑥 ≈ 𝐴) | 
| 40 |  | isnumi 9986 | . . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → 𝐴 ∈ dom card) | 
| 41 | 39, 40 | sylan2 593 | . . . . . 6
⊢ ((𝑥 ∈ On ∧ (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) → 𝐴 ∈ dom card) | 
| 42 | 41 | rexlimiva 3147 | . . . . 5
⊢
(∃𝑥 ∈ On
(𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴 → 𝐴 ∈ dom card) | 
| 43 | 38, 42 | syl6 35 | . . . 4
⊢ (𝐴 ∈ V → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → 𝐴 ∈ dom card)) | 
| 44 | 36, 43 | syld 47 | . . 3
⊢ (𝐴 ∈ V → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | 
| 45 | 1, 44 | syl 17 | . 2
⊢ (𝐴 ∈ 𝐶 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | 
| 46 | 45 | exlimdv 1933 | 1
⊢ (𝐴 ∈ 𝐶 → (∃𝑔∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) |