| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝑌 → (𝑎𝐹𝑠) = (𝑌𝐹𝑠)) |
| 2 | | 2fveq3 6911 |
. . 3
⊢ (𝑎 = 𝑌 → (𝐻‘(card‘𝑎)) = (𝐻‘(card‘𝑌))) |
| 3 | 1, 2 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑌 → ((𝑎𝐹𝑠) = (𝐻‘(card‘𝑎)) ↔ (𝑌𝐹𝑠) = (𝐻‘(card‘𝑌)))) |
| 4 | | oveq2 7439 |
. . 3
⊢ (𝑠 = 𝑅 → (𝑌𝐹𝑠) = (𝑌𝐹𝑅)) |
| 5 | 4 | eqeq1d 2739 |
. 2
⊢ (𝑠 = 𝑅 → ((𝑌𝐹𝑠) = (𝐻‘(card‘𝑌)) ↔ (𝑌𝐹𝑅) = (𝐻‘(card‘𝑌)))) |
| 6 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑥𝑎 |
| 7 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑟𝑎 |
| 8 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑟𝑠 |
| 9 | | pwfseqlem4.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
| 10 | | nfmpo1 7513 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
| 11 | 9, 10 | nfcxfr 2903 |
. . . . 5
⊢
Ⅎ𝑥𝐹 |
| 12 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥𝑟 |
| 13 | 6, 11, 12 | nfov 7461 |
. . . 4
⊢
Ⅎ𝑥(𝑎𝐹𝑟) |
| 14 | 13 | nfeq1 2921 |
. . 3
⊢
Ⅎ𝑥(𝑎𝐹𝑟) = (𝐻‘(card‘𝑎)) |
| 15 | | nfmpo2 7514 |
. . . . . 6
⊢
Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
| 16 | 9, 15 | nfcxfr 2903 |
. . . . 5
⊢
Ⅎ𝑟𝐹 |
| 17 | 7, 16, 8 | nfov 7461 |
. . . 4
⊢
Ⅎ𝑟(𝑎𝐹𝑠) |
| 18 | 17 | nfeq1 2921 |
. . 3
⊢
Ⅎ𝑟(𝑎𝐹𝑠) = (𝐻‘(card‘𝑎)) |
| 19 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟)) |
| 20 | | 2fveq3 6911 |
. . . 4
⊢ (𝑥 = 𝑎 → (𝐻‘(card‘𝑥)) = (𝐻‘(card‘𝑎))) |
| 21 | 19, 20 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) = (𝐻‘(card‘𝑥)) ↔ (𝑎𝐹𝑟) = (𝐻‘(card‘𝑎)))) |
| 22 | | oveq2 7439 |
. . . 4
⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠)) |
| 23 | 22 | eqeq1d 2739 |
. . 3
⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) = (𝐻‘(card‘𝑎)) ↔ (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎)))) |
| 24 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 25 | | vex 3484 |
. . . . . 6
⊢ 𝑟 ∈ V |
| 26 | | fvex 6919 |
. . . . . . 7
⊢ (𝐻‘(card‘𝑥)) ∈ V |
| 27 | | fvex 6919 |
. . . . . . 7
⊢ (𝐷‘∩ {𝑧
∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}) ∈ V |
| 28 | 26, 27 | ifex 4576 |
. . . . . 6
⊢ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥})) ∈ V |
| 29 | 9 | ovmpt4g 7580 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ 𝑟 ∈ V ∧ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥})) ∈ V) → (𝑥𝐹𝑟) = if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
| 30 | 24, 25, 28, 29 | mp3an 1463 |
. . . . 5
⊢ (𝑥𝐹𝑟) = if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥})) |
| 31 | | iftrue 4531 |
. . . . 5
⊢ (𝑥 ∈ Fin → if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥})) = (𝐻‘(card‘𝑥))) |
| 32 | 30, 31 | eqtrid 2789 |
. . . 4
⊢ (𝑥 ∈ Fin → (𝑥𝐹𝑟) = (𝐻‘(card‘𝑥))) |
| 33 | 32 | adantr 480 |
. . 3
⊢ ((𝑥 ∈ Fin ∧ 𝑟 ∈ 𝑉) → (𝑥𝐹𝑟) = (𝐻‘(card‘𝑥))) |
| 34 | 6, 7, 8, 14, 18, 21, 23, 33 | vtocl2gaf 3579 |
. 2
⊢ ((𝑎 ∈ Fin ∧ 𝑠 ∈ 𝑉) → (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎))) |
| 35 | 3, 5, 34 | vtocl2ga 3578 |
1
⊢ ((𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑌𝐹𝑅) = (𝐻‘(card‘𝑌))) |