| Step | Hyp | Ref
| Expression |
| 1 | | en1 9064 |
. . 3
⊢ (𝐹 ≈ 1o ↔
∃𝑝 𝐹 = {𝑝}) |
| 2 | | funrel 6583 |
. . . . . . . 8
⊢ (Fun
{𝑝} → Rel {𝑝}) |
| 3 | | vsnid 4663 |
. . . . . . . 8
⊢ 𝑝 ∈ {𝑝} |
| 4 | | elrel 5808 |
. . . . . . . 8
⊢ ((Rel
{𝑝} ∧ 𝑝 ∈ {𝑝}) → ∃𝑥∃𝑦 𝑝 = 〈𝑥, 𝑦〉) |
| 5 | 2, 3, 4 | sylancl 586 |
. . . . . . 7
⊢ (Fun
{𝑝} → ∃𝑥∃𝑦 𝑝 = 〈𝑥, 𝑦〉) |
| 6 | | sneq 4636 |
. . . . . . . 8
⊢ (𝑝 = 〈𝑥, 𝑦〉 → {𝑝} = {〈𝑥, 𝑦〉}) |
| 7 | 6 | 2eximi 1836 |
. . . . . . 7
⊢
(∃𝑥∃𝑦 𝑝 = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦{𝑝} = {〈𝑥, 𝑦〉}) |
| 8 | 5, 7 | syl 17 |
. . . . . 6
⊢ (Fun
{𝑝} → ∃𝑥∃𝑦{𝑝} = {〈𝑥, 𝑦〉}) |
| 9 | | funcnvsn 6616 |
. . . . . . 7
⊢ Fun ◡{〈𝑥, 𝑦〉} |
| 10 | 9 | gen2 1796 |
. . . . . 6
⊢
∀𝑥∀𝑦Fun ◡{〈𝑥, 𝑦〉} |
| 11 | | 19.29r2 1875 |
. . . . . . 7
⊢
((∃𝑥∃𝑦{𝑝} = {〈𝑥, 𝑦〉} ∧ ∀𝑥∀𝑦Fun ◡{〈𝑥, 𝑦〉}) → ∃𝑥∃𝑦({𝑝} = {〈𝑥, 𝑦〉} ∧ Fun ◡{〈𝑥, 𝑦〉})) |
| 12 | | cnveq 5884 |
. . . . . . . . . 10
⊢ ({𝑝} = {〈𝑥, 𝑦〉} → ◡{𝑝} = ◡{〈𝑥, 𝑦〉}) |
| 13 | 12 | funeqd 6588 |
. . . . . . . . 9
⊢ ({𝑝} = {〈𝑥, 𝑦〉} → (Fun ◡{𝑝} ↔ Fun ◡{〈𝑥, 𝑦〉})) |
| 14 | 13 | biimpar 477 |
. . . . . . . 8
⊢ (({𝑝} = {〈𝑥, 𝑦〉} ∧ Fun ◡{〈𝑥, 𝑦〉}) → Fun ◡{𝑝}) |
| 15 | 14 | exlimivv 1932 |
. . . . . . 7
⊢
(∃𝑥∃𝑦({𝑝} = {〈𝑥, 𝑦〉} ∧ Fun ◡{〈𝑥, 𝑦〉}) → Fun ◡{𝑝}) |
| 16 | 11, 15 | syl 17 |
. . . . . 6
⊢
((∃𝑥∃𝑦{𝑝} = {〈𝑥, 𝑦〉} ∧ ∀𝑥∀𝑦Fun ◡{〈𝑥, 𝑦〉}) → Fun ◡{𝑝}) |
| 17 | 8, 10, 16 | sylancl 586 |
. . . . 5
⊢ (Fun
{𝑝} → Fun ◡{𝑝}) |
| 18 | 17 | ax-gen 1795 |
. . . 4
⊢
∀𝑝(Fun {𝑝} → Fun ◡{𝑝}) |
| 19 | | 19.29r 1874 |
. . . . 5
⊢
((∃𝑝 𝐹 = {𝑝} ∧ ∀𝑝(Fun {𝑝} → Fun ◡{𝑝})) → ∃𝑝(𝐹 = {𝑝} ∧ (Fun {𝑝} → Fun ◡{𝑝}))) |
| 20 | | funeq 6586 |
. . . . . . . 8
⊢ (𝐹 = {𝑝} → (Fun 𝐹 ↔ Fun {𝑝})) |
| 21 | | cnveq 5884 |
. . . . . . . . 9
⊢ (𝐹 = {𝑝} → ◡𝐹 = ◡{𝑝}) |
| 22 | 21 | funeqd 6588 |
. . . . . . . 8
⊢ (𝐹 = {𝑝} → (Fun ◡𝐹 ↔ Fun ◡{𝑝})) |
| 23 | 20, 22 | imbi12d 344 |
. . . . . . 7
⊢ (𝐹 = {𝑝} → ((Fun 𝐹 → Fun ◡𝐹) ↔ (Fun {𝑝} → Fun ◡{𝑝}))) |
| 24 | 23 | biimpar 477 |
. . . . . 6
⊢ ((𝐹 = {𝑝} ∧ (Fun {𝑝} → Fun ◡{𝑝})) → (Fun 𝐹 → Fun ◡𝐹)) |
| 25 | 24 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑝(𝐹 = {𝑝} ∧ (Fun {𝑝} → Fun ◡{𝑝})) → (Fun 𝐹 → Fun ◡𝐹)) |
| 26 | 19, 25 | syl 17 |
. . . 4
⊢
((∃𝑝 𝐹 = {𝑝} ∧ ∀𝑝(Fun {𝑝} → Fun ◡{𝑝})) → (Fun 𝐹 → Fun ◡𝐹)) |
| 27 | 18, 26 | mpan2 691 |
. . 3
⊢
(∃𝑝 𝐹 = {𝑝} → (Fun 𝐹 → Fun ◡𝐹)) |
| 28 | 1, 27 | sylbi 217 |
. 2
⊢ (𝐹 ≈ 1o →
(Fun 𝐹 → Fun ◡𝐹)) |
| 29 | 28 | impcom 407 |
1
⊢ ((Fun
𝐹 ∧ 𝐹 ≈ 1o) → Fun ◡𝐹) |