Step | Hyp | Ref
| Expression |
1 | | indf1o 29413 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑𝑚 𝑂)) |
2 | | f1of1 6049 |
. . . 4
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑𝑚 𝑂) → (𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑𝑚 𝑂)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑𝑚 𝑂)) |
4 | | inss1 3795 |
. . 3
⊢
(𝒫 𝑂 ∩
Fin) ⊆ 𝒫 𝑂 |
5 | | f1ores 6064 |
. . 3
⊢
(((𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑𝑚 𝑂) ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫
𝑂) →
((𝟭‘𝑂)
↾ (𝒫 𝑂 ∩
Fin)):(𝒫 𝑂 ∩
Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
6 | 3, 4, 5 | sylancl 693 |
. 2
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
7 | | resres 5329 |
. . . 4
⊢
(((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) |
8 | | f1ofn 6051 |
. . . . . 6
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑𝑚 𝑂) → (𝟭‘𝑂) Fn 𝒫 𝑂) |
9 | | fnresdm 5914 |
. . . . . 6
⊢
((𝟭‘𝑂)
Fn 𝒫 𝑂 →
((𝟭‘𝑂)
↾ 𝒫 𝑂) =
(𝟭‘𝑂)) |
10 | 1, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂)) |
11 | 10 | reseq1d 5316 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ Fin)) |
12 | 7, 11 | syl5eqr 2658 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) = ((𝟭‘𝑂) ↾ Fin)) |
13 | | eqidd 2611 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂 ∩ Fin) = (𝒫 𝑂 ∩ Fin)) |
14 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑂 ∈ 𝑉) |
15 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) |
16 | 4, 15 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ 𝒫 𝑂) |
17 | 16 | elpwid 4118 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ⊆ 𝑂) |
18 | | indf 29405 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
19 | 17, 18 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔) |
22 | 21 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1} ↔ 𝑔:𝑂⟶{0, 1})) |
23 | 20, 22 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔:𝑂⟶{0, 1}) |
24 | | prex 4836 |
. . . . . . . . . . . 12
⊢ {0, 1}
∈ V |
25 | | elmapg 7757 |
. . . . . . . . . . . 12
⊢ (({0, 1}
∈ V ∧ 𝑂 ∈
𝑉) → (𝑔 ∈ ({0, 1}
↑𝑚 𝑂) ↔ 𝑔:𝑂⟶{0, 1})) |
26 | 24, 25 | mpan 702 |
. . . . . . . . . . 11
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ↔ 𝑔:𝑂⟶{0, 1})) |
27 | 26 | biimpar 501 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 ∈ ({0, 1} ↑𝑚
𝑂)) |
28 | 14, 23, 27 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔 ∈ ({0, 1} ↑𝑚
𝑂)) |
29 | 21 | cnveqd 5220 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ◡((𝟭‘𝑂)‘𝑎) = ◡𝑔) |
30 | 29 | imaeq1d 5384 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = (◡𝑔 “ {1})) |
31 | | indpi1 29411 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
32 | 17, 31 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
33 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑂 ∩
Fin) ⊆ Fin |
34 | 33, 15 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ Fin) |
35 | 32, 34 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
36 | 35 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
37 | 30, 36 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡𝑔 “ {1}) ∈ Fin) |
38 | 28, 37 | jca 553 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) |
39 | 38 | ex 449 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
40 | 39 | rexlimdva 3013 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
41 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡𝑔 “ {1}) ⊆ dom 𝑔 |
42 | 26 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑𝑚
𝑂)) → 𝑔:𝑂⟶{0, 1}) |
43 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑔:𝑂⟶{0, 1} → dom 𝑔 = 𝑂) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑𝑚
𝑂)) → dom 𝑔 = 𝑂) |
45 | 44 | adantrr 749 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → dom 𝑔 = 𝑂) |
46 | 41, 45 | syl5sseq 3616 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ⊆ 𝑂) |
47 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ Fin) |
48 | | elfpw 8151 |
. . . . . . . . 9
⊢ ((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ↔ ((◡𝑔 “ {1}) ⊆ 𝑂 ∧ (◡𝑔 “ {1}) ∈ Fin)) |
49 | 46, 47, 48 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin)) |
50 | | indpreima 29414 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 = ((𝟭‘𝑂)‘(◡𝑔 “ {1}))) |
51 | 50 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
52 | 42, 51 | syldan 486 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑𝑚
𝑂)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
53 | 52 | adantrr 749 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
54 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = (◡𝑔 “ {1}) → ((𝟭‘𝑂)‘𝑎) = ((𝟭‘𝑂)‘(◡𝑔 “ {1}))) |
55 | 54 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝑔 “ {1}) → (((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ ((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔)) |
56 | 55 | rspcev 3282 |
. . . . . . . 8
⊢ (((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ∧
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
57 | 49, 53, 56 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
∃𝑎 ∈ (𝒫
𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
58 | 57 | ex 449 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → ((𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin) → ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
59 | 40, 58 | impbid 201 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ (𝑔 ∈ ({0, 1} ↑𝑚
𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
60 | 1, 8 | syl 17 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) Fn 𝒫 𝑂) |
61 | | fvelimab 6163 |
. . . . . 6
⊢
(((𝟭‘𝑂) Fn 𝒫 𝑂 ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
62 | 60, 4, 61 | sylancl 693 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
63 | | cnveq 5218 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ◡𝑓 = ◡𝑔) |
64 | 63 | imaeq1d 5384 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (◡𝑓 “ {1}) = (◡𝑔 “ {1})) |
65 | 64 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → ((◡𝑓 “ {1}) ∈ Fin ↔ (◡𝑔 “ {1}) ∈ Fin)) |
66 | 65 | elrab 3331 |
. . . . . 6
⊢ (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1}
↑𝑚 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) |
67 | 66 | a1i 11 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1}
↑𝑚 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
68 | 59, 62, 67 | 3bitr4d 299 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ 𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
69 | 68 | eqrdv 2608 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) = {𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |
70 | 12, 13, 69 | f1oeq123d 6046 |
. 2
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
71 | 6, 70 | mpbid 221 |
1
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚
𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |