Proof of Theorem k0004lem3
| Step | Hyp | Ref
| Expression |
| 1 | | sneq 4636 |
. . . . . 6
⊢ ((𝐹‘𝐴) = 𝐶 → {(𝐹‘𝐴)} = {𝐶}) |
| 2 | | eqimss 4042 |
. . . . . 6
⊢ ({(𝐹‘𝐴)} = {𝐶} → {(𝐹‘𝐴)} ⊆ {𝐶}) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝐹‘𝐴) = 𝐶 → {(𝐹‘𝐴)} ⊆ {𝐶}) |
| 4 | | fvex 6919 |
. . . . . 6
⊢ (𝐹‘𝐴) ∈ V |
| 5 | 4 | snsssn 4841 |
. . . . 5
⊢ ({(𝐹‘𝐴)} ⊆ {𝐶} → (𝐹‘𝐴) = 𝐶) |
| 6 | 3, 5 | impbii 209 |
. . . 4
⊢ ((𝐹‘𝐴) = 𝐶 ↔ {(𝐹‘𝐴)} ⊆ {𝐶}) |
| 7 | | elmapfn 8905 |
. . . . . 6
⊢ (𝐹 ∈ (𝐵 ↑m {𝐴}) → 𝐹 Fn {𝐴}) |
| 8 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → 𝐴 ∈ 𝑈) |
| 9 | | snidg 4660 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ {𝐴}) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → 𝐴 ∈ {𝐴}) |
| 11 | | fnsnfv 6988 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴} ∧ 𝐴 ∈ {𝐴}) → {(𝐹‘𝐴)} = (𝐹 “ {𝐴})) |
| 12 | 7, 10, 11 | syl2an2 686 |
. . . . 5
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → {(𝐹‘𝐴)} = (𝐹 “ {𝐴})) |
| 13 | 12 | sseq1d 4015 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → ({(𝐹‘𝐴)} ⊆ {𝐶} ↔ (𝐹 “ {𝐴}) ⊆ {𝐶})) |
| 14 | 6, 13 | bitrid 283 |
. . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹 “ {𝐴}) ⊆ {𝐶})) |
| 15 | 14 | pm5.32da 579 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ (𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}))) |
| 16 | | snex 5436 |
. . 3
⊢ {𝐴} ∈ V |
| 17 | | simp2 1138 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ 𝑉) |
| 18 | | simp3 1139 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
| 19 | 18 | snssd 4809 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) |
| 20 | | k0004lem2 44161 |
. . 3
⊢ (({𝐴} ∈ V ∧ 𝐵 ∈ 𝑉 ∧ {𝐶} ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}) ↔ 𝐹 ∈ ({𝐶} ↑m {𝐴}))) |
| 21 | 16, 17, 19, 20 | mp3an2i 1468 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}) ↔ 𝐹 ∈ ({𝐶} ↑m {𝐴}))) |
| 22 | | snex 5436 |
. . . 4
⊢ {𝐶} ∈ V |
| 23 | 22, 16 | elmap 8911 |
. . 3
⊢ (𝐹 ∈ ({𝐶} ↑m {𝐴}) ↔ 𝐹:{𝐴}⟶{𝐶}) |
| 24 | | fsng 7157 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝐵) → (𝐹:{𝐴}⟶{𝐶} ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
| 25 | 24 | 3adant2 1132 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐹:{𝐴}⟶{𝐶} ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
| 26 | 23, 25 | bitrid 283 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐹 ∈ ({𝐶} ↑m {𝐴}) ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
| 27 | 15, 21, 26 | 3bitrd 305 |
1
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ 𝐹 = {〈𝐴, 𝐶〉})) |