Step | Hyp | Ref
| Expression |
1 | | indf1o 31575 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)) |
2 | | f1of1 6630 |
. . . 4
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)
→ (𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑m 𝑂)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑m 𝑂)) |
4 | | inss1 4129 |
. . 3
⊢
(𝒫 𝑂 ∩
Fin) ⊆ 𝒫 𝑂 |
5 | | f1ores 6645 |
. . 3
⊢
(((𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑m 𝑂) ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
6 | 3, 4, 5 | sylancl 589 |
. 2
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
7 | | resres 5848 |
. . . 4
⊢
(((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) |
8 | | f1ofn 6632 |
. . . . . 6
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)
→ (𝟭‘𝑂)
Fn 𝒫 𝑂) |
9 | | fnresdm 6466 |
. . . . . 6
⊢
((𝟭‘𝑂)
Fn 𝒫 𝑂 →
((𝟭‘𝑂)
↾ 𝒫 𝑂) =
(𝟭‘𝑂)) |
10 | 1, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂)) |
11 | 10 | reseq1d 5834 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ Fin)) |
12 | 7, 11 | eqtr3id 2788 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) = ((𝟭‘𝑂) ↾ Fin)) |
13 | | eqidd 2740 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂 ∩ Fin) = (𝒫 𝑂 ∩ Fin)) |
14 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑂 ∈ 𝑉) |
15 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) |
16 | 4, 15 | sseldi 3885 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ 𝒫 𝑂) |
17 | 16 | elpwid 4509 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ⊆ 𝑂) |
18 | | indf 31566 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
19 | 17, 18 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
20 | 19 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
21 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔) |
22 | 21 | feq1d 6500 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1} ↔ 𝑔:𝑂⟶{0, 1})) |
23 | 20, 22 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔:𝑂⟶{0, 1}) |
24 | | prex 5309 |
. . . . . . . . . . 11
⊢ {0, 1}
∈ V |
25 | | elmapg 8463 |
. . . . . . . . . . 11
⊢ (({0, 1}
∈ V ∧ 𝑂 ∈
𝑉) → (𝑔 ∈ ({0, 1}
↑m 𝑂)
↔ 𝑔:𝑂⟶{0, 1})) |
26 | 24, 25 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ↔ 𝑔:𝑂⟶{0, 1})) |
27 | 26 | biimpar 481 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
28 | 14, 23, 27 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
29 | 21 | cnveqd 5728 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ◡((𝟭‘𝑂)‘𝑎) = ◡𝑔) |
30 | 29 | imaeq1d 5912 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = (◡𝑔 “ {1})) |
31 | | indpi1 31571 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
32 | 17, 31 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
33 | | inss2 4130 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑂 ∩
Fin) ⊆ Fin |
34 | 33, 15 | sseldi 3885 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ Fin) |
35 | 32, 34 | eqeltrd 2834 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
36 | 35 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
37 | 30, 36 | eqeltrrd 2835 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡𝑔 “ {1}) ∈ Fin) |
38 | 28, 37 | jca 515 |
. . . . . . 7
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) |
39 | 38 | rexlimdva2 3198 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
40 | | cnvimass 5933 |
. . . . . . . . . 10
⊢ (◡𝑔 “ {1}) ⊆ dom 𝑔 |
41 | 26 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → 𝑔:𝑂⟶{0, 1}) |
42 | 41 | fdmd 6526 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → dom 𝑔 = 𝑂) |
43 | 42 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → dom 𝑔 = 𝑂) |
44 | 40, 43 | sseqtrid 3939 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ⊆ 𝑂) |
45 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ Fin) |
46 | | elfpw 8912 |
. . . . . . . . 9
⊢ ((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ↔ ((◡𝑔 “ {1}) ⊆ 𝑂 ∧ (◡𝑔 “ {1}) ∈ Fin)) |
47 | 44, 45, 46 | sylanbrc 586 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin)) |
48 | | indpreima 31576 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 = ((𝟭‘𝑂)‘(◡𝑔 “ {1}))) |
49 | 48 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
50 | 41, 49 | syldan 594 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
51 | 50 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
52 | | fveqeq2 6696 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝑔 “ {1}) → (((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ ((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔)) |
53 | 52 | rspcev 3529 |
. . . . . . . 8
⊢ (((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ∧
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
54 | 47, 51, 53 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
∃𝑎 ∈ (𝒫
𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
55 | 54 | ex 416 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → ((𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin) → ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
56 | 39, 55 | impbid 215 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
57 | 1, 8 | syl 17 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) Fn 𝒫 𝑂) |
58 | | fvelimab 6754 |
. . . . . 6
⊢
(((𝟭‘𝑂) Fn 𝒫 𝑂 ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
59 | 57, 4, 58 | sylancl 589 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
60 | | cnveq 5726 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ◡𝑓 = ◡𝑔) |
61 | 60 | imaeq1d 5912 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (◡𝑓 “ {1}) = (◡𝑔 “ {1})) |
62 | 61 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → ((◡𝑓 “ {1}) ∈ Fin ↔ (◡𝑔 “ {1}) ∈ Fin)) |
63 | 62 | elrab 3593 |
. . . . . 6
⊢ (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1}
↑m 𝑂) ∧
(◡𝑔 “ {1}) ∈ Fin)) |
64 | 63 | a1i 11 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1}
↑m 𝑂) ∧
(◡𝑔 “ {1}) ∈ Fin))) |
65 | 56, 59, 64 | 3bitr4d 314 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ 𝑔 ∈ {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
66 | 65 | eqrdv 2737 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) = {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |
67 | 12, 13, 66 | f1oeq123d 6625 |
. 2
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
68 | 6, 67 | mpbid 235 |
1
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |