Proof of Theorem k0004lem3
Step | Hyp | Ref
| Expression |
1 | | sneq 4526 |
. . . . . 6
⊢ ((𝐹‘𝐴) = 𝐶 → {(𝐹‘𝐴)} = {𝐶}) |
2 | | eqimss 3933 |
. . . . . 6
⊢ ({(𝐹‘𝐴)} = {𝐶} → {(𝐹‘𝐴)} ⊆ {𝐶}) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝐹‘𝐴) = 𝐶 → {(𝐹‘𝐴)} ⊆ {𝐶}) |
4 | | fvex 6687 |
. . . . . 6
⊢ (𝐹‘𝐴) ∈ V |
5 | 4 | snsssn 4727 |
. . . . 5
⊢ ({(𝐹‘𝐴)} ⊆ {𝐶} → (𝐹‘𝐴) = 𝐶) |
6 | 3, 5 | impbii 212 |
. . . 4
⊢ ((𝐹‘𝐴) = 𝐶 ↔ {(𝐹‘𝐴)} ⊆ {𝐶}) |
7 | | elmapfn 8475 |
. . . . . 6
⊢ (𝐹 ∈ (𝐵 ↑m {𝐴}) → 𝐹 Fn {𝐴}) |
8 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → 𝐴 ∈ 𝑈) |
9 | | snidg 4550 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ {𝐴}) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → 𝐴 ∈ {𝐴}) |
11 | | fnsnfv 6747 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴} ∧ 𝐴 ∈ {𝐴}) → {(𝐹‘𝐴)} = (𝐹 “ {𝐴})) |
12 | 7, 10, 11 | syl2an2 686 |
. . . . 5
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → {(𝐹‘𝐴)} = (𝐹 “ {𝐴})) |
13 | 12 | sseq1d 3908 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → ({(𝐹‘𝐴)} ⊆ {𝐶} ↔ (𝐹 “ {𝐴}) ⊆ {𝐶})) |
14 | 6, 13 | syl5bb 286 |
. . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) ∧ 𝐹 ∈ (𝐵 ↑m {𝐴})) → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹 “ {𝐴}) ⊆ {𝐶})) |
15 | 14 | pm5.32da 582 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ (𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}))) |
16 | | snex 5298 |
. . 3
⊢ {𝐴} ∈ V |
17 | | simp2 1138 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ 𝑉) |
18 | | simp3 1139 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
19 | 18 | snssd 4697 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) |
20 | | k0004lem2 41304 |
. . 3
⊢ (({𝐴} ∈ V ∧ 𝐵 ∈ 𝑉 ∧ {𝐶} ⊆ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}) ↔ 𝐹 ∈ ({𝐶} ↑m {𝐴}))) |
21 | 16, 17, 19, 20 | mp3an2i 1467 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹 “ {𝐴}) ⊆ {𝐶}) ↔ 𝐹 ∈ ({𝐶} ↑m {𝐴}))) |
22 | | snex 5298 |
. . . 4
⊢ {𝐶} ∈ V |
23 | 22, 16 | elmap 8481 |
. . 3
⊢ (𝐹 ∈ ({𝐶} ↑m {𝐴}) ↔ 𝐹:{𝐴}⟶{𝐶}) |
24 | | fsng 6909 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝐵) → (𝐹:{𝐴}⟶{𝐶} ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
25 | 24 | 3adant2 1132 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐹:{𝐴}⟶{𝐶} ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
26 | 23, 25 | syl5bb 286 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐹 ∈ ({𝐶} ↑m {𝐴}) ↔ 𝐹 = {〈𝐴, 𝐶〉})) |
27 | 15, 21, 26 | 3bitrd 308 |
1
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∈ (𝐵 ↑m {𝐴}) ∧ (𝐹‘𝐴) = 𝐶) ↔ 𝐹 = {〈𝐴, 𝐶〉})) |