| Step | Hyp | Ref
| Expression |
| 1 | | cnveq 5884 |
. . 3
⊢ (𝑥 = ∅ → ◡𝑥 = ◡∅) |
| 2 | 1 | eleq1d 2826 |
. 2
⊢ (𝑥 = ∅ → (◡𝑥 ∈ Fin ↔ ◡∅ ∈ Fin)) |
| 3 | | cnveq 5884 |
. . 3
⊢ (𝑥 = 𝑦 → ◡𝑥 = ◡𝑦) |
| 4 | 3 | eleq1d 2826 |
. 2
⊢ (𝑥 = 𝑦 → (◡𝑥 ∈ Fin ↔ ◡𝑦 ∈ Fin)) |
| 5 | | cnveq 5884 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ◡𝑥 = ◡(𝑦 ∪ {𝑧})) |
| 6 | 5 | eleq1d 2826 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (◡𝑥 ∈ Fin ↔ ◡(𝑦 ∪ {𝑧}) ∈ Fin)) |
| 7 | | cnveq 5884 |
. . 3
⊢ (𝑥 = 𝐴 → ◡𝑥 = ◡𝐴) |
| 8 | 7 | eleq1d 2826 |
. 2
⊢ (𝑥 = 𝐴 → (◡𝑥 ∈ Fin ↔ ◡𝐴 ∈ Fin)) |
| 9 | | cnv0 6160 |
. . 3
⊢ ◡∅ = ∅ |
| 10 | | 0fi 9082 |
. . 3
⊢ ∅
∈ Fin |
| 11 | 9, 10 | eqeltri 2837 |
. 2
⊢ ◡∅ ∈ Fin |
| 12 | | cnvun 6162 |
. . . 4
⊢ ◡(𝑦 ∪ {𝑧}) = (◡𝑦 ∪ ◡{𝑧}) |
| 13 | | elvv 5760 |
. . . . . . 7
⊢ (𝑧 ∈ (V × V) ↔
∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉) |
| 14 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑢, 𝑣〉 → {𝑧} = {〈𝑢, 𝑣〉}) |
| 15 | | cnveq 5884 |
. . . . . . . . . . 11
⊢ ({𝑧} = {〈𝑢, 𝑣〉} → ◡{𝑧} = ◡{〈𝑢, 𝑣〉}) |
| 16 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
| 17 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
| 18 | 16, 17 | cnvsn 6246 |
. . . . . . . . . . 11
⊢ ◡{〈𝑢, 𝑣〉} = {〈𝑣, 𝑢〉} |
| 19 | 15, 18 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ({𝑧} = {〈𝑢, 𝑣〉} → ◡{𝑧} = {〈𝑣, 𝑢〉}) |
| 20 | 14, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ◡{𝑧} = {〈𝑣, 𝑢〉}) |
| 21 | | snfi 9083 |
. . . . . . . . 9
⊢
{〈𝑣, 𝑢〉} ∈
Fin |
| 22 | 20, 21 | eqeltrdi 2849 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ◡{𝑧} ∈ Fin) |
| 23 | 22 | exlimivv 1932 |
. . . . . . 7
⊢
(∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉 → ◡{𝑧} ∈ Fin) |
| 24 | 13, 23 | sylbi 217 |
. . . . . 6
⊢ (𝑧 ∈ (V × V) →
◡{𝑧} ∈ Fin) |
| 25 | | dfdm4 5906 |
. . . . . . . . 9
⊢ dom
{𝑧} = ran ◡{𝑧} |
| 26 | | dmsnn0 6227 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (V × V) ↔ dom
{𝑧} ≠
∅) |
| 27 | 26 | biimpri 228 |
. . . . . . . . . 10
⊢ (dom
{𝑧} ≠ ∅ →
𝑧 ∈ (V ×
V)) |
| 28 | 27 | necon1bi 2969 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ (V × V)
→ dom {𝑧} =
∅) |
| 29 | 25, 28 | eqtr3id 2791 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ (V × V)
→ ran ◡{𝑧} = ∅) |
| 30 | | relcnv 6122 |
. . . . . . . . 9
⊢ Rel ◡{𝑧} |
| 31 | | relrn0 5983 |
. . . . . . . . 9
⊢ (Rel
◡{𝑧} → (◡{𝑧} = ∅ ↔ ran ◡{𝑧} = ∅)) |
| 32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
⊢ (◡{𝑧} = ∅ ↔ ran ◡{𝑧} = ∅) |
| 33 | 29, 32 | sylibr 234 |
. . . . . . 7
⊢ (¬
𝑧 ∈ (V × V)
→ ◡{𝑧} = ∅) |
| 34 | 33, 10 | eqeltrdi 2849 |
. . . . . 6
⊢ (¬
𝑧 ∈ (V × V)
→ ◡{𝑧} ∈ Fin) |
| 35 | 24, 34 | pm2.61i 182 |
. . . . 5
⊢ ◡{𝑧} ∈ Fin |
| 36 | | unfi 9211 |
. . . . 5
⊢ ((◡𝑦 ∈ Fin ∧ ◡{𝑧} ∈ Fin) → (◡𝑦 ∪ ◡{𝑧}) ∈ Fin) |
| 37 | 35, 36 | mpan2 691 |
. . . 4
⊢ (◡𝑦 ∈ Fin → (◡𝑦 ∪ ◡{𝑧}) ∈ Fin) |
| 38 | 12, 37 | eqeltrid 2845 |
. . 3
⊢ (◡𝑦 ∈ Fin → ◡(𝑦 ∪ {𝑧}) ∈ Fin) |
| 39 | 38 | a1i 11 |
. 2
⊢ (𝑦 ∈ Fin → (◡𝑦 ∈ Fin → ◡(𝑦 ∪ {𝑧}) ∈ Fin)) |
| 40 | 2, 4, 6, 8, 11, 39 | findcard2 9204 |
1
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) |