Step | Hyp | Ref
| Expression |
1 | | indf1o 31992 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)) |
2 | | f1of1 6715 |
. . . 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 4162 |
. . 3
⊢
(𝒫 𝑂 ∩
Fin) ⊆ 𝒫 𝑂 |
5 | | f1ores 6730 |
. . 3
⊢
(((𝟭‘𝑂):𝒫 𝑂–1-1→({0, 1} ↑m 𝑂) ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
6 | 3, 4, 5 | sylancl 586 |
. 2
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin))) |
7 | | resres 5904 |
. . . 4
⊢
(((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) |
8 | | f1ofn 6717 |
. . . . . 6
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)
→ (𝟭‘𝑂)
Fn 𝒫 𝑂) |
9 | | fnresdm 6551 |
. . . . . 6
⊢
((𝟭‘𝑂)
Fn 𝒫 𝑂 →
((𝟭‘𝑂)
↾ 𝒫 𝑂) =
(𝟭‘𝑂)) |
10 | 1, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂)) |
11 | 10 | reseq1d 5890 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ Fin)) |
12 | 7, 11 | eqtr3id 2792 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) = ((𝟭‘𝑂) ↾ Fin)) |
13 | | eqidd 2739 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂 ∩ Fin) = (𝒫 𝑂 ∩ Fin)) |
14 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑂 ∈ 𝑉) |
15 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) |
16 | 4, 15 | sselid 3919 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ 𝒫 𝑂) |
17 | 16 | elpwid 4544 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ⊆ 𝑂) |
18 | | indf 31983 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
19 | 17, 18 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
21 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔) |
22 | 21 | feq1d 6585 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1} ↔ 𝑔:𝑂⟶{0, 1})) |
23 | 20, 22 | mpbid 231 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔:𝑂⟶{0, 1}) |
24 | | prex 5355 |
. . . . . . . . . . 11
⊢ {0, 1}
∈ V |
25 | | elmapg 8628 |
. . . . . . . . . . 11
⊢ (({0, 1}
∈ V ∧ 𝑂 ∈
𝑉) → (𝑔 ∈ ({0, 1}
↑m 𝑂)
↔ 𝑔:𝑂⟶{0, 1})) |
26 | 24, 25 | mpan 687 |
. . . . . . . . . 10
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ↔ 𝑔:𝑂⟶{0, 1})) |
27 | 26 | biimpar 478 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
28 | 14, 23, 27 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
29 | 21 | cnveqd 5784 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ◡((𝟭‘𝑂)‘𝑎) = ◡𝑔) |
30 | 29 | imaeq1d 5968 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = (◡𝑔 “ {1})) |
31 | | indpi1 31988 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
32 | 17, 31 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
33 | | inss2 4163 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑂 ∩
Fin) ⊆ Fin |
34 | 33, 15 | sselid 3919 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ Fin) |
35 | 32, 34 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
36 | 35 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
37 | 30, 36 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡𝑔 “ {1}) ∈ Fin) |
38 | 28, 37 | jca 512 |
. . . . . . 7
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) |
39 | 38 | rexlimdva2 3216 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
40 | | cnvimass 5989 |
. . . . . . . . . 10
⊢ (◡𝑔 “ {1}) ⊆ dom 𝑔 |
41 | 26 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → 𝑔:𝑂⟶{0, 1}) |
42 | 41 | fdmd 6611 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → dom 𝑔 = 𝑂) |
43 | 42 | adantrr 714 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → dom 𝑔 = 𝑂) |
44 | 40, 43 | sseqtrid 3973 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ⊆ 𝑂) |
45 | | simprr 770 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ Fin) |
46 | | elfpw 9121 |
. . . . . . . . 9
⊢ ((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ↔ ((◡𝑔 “ {1}) ⊆ 𝑂 ∧ (◡𝑔 “ {1}) ∈ Fin)) |
47 | 44, 45, 46 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin)) |
48 | | indpreima 31993 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 = ((𝟭‘𝑂)‘(◡𝑔 “ {1}))) |
49 | 48 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
50 | 41, 49 | syldan 591 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
51 | 50 | adantrr 714 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
52 | | fveqeq2 6783 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝑔 “ {1}) → (((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ ((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔)) |
53 | 52 | rspcev 3561 |
. . . . . . . 8
⊢ (((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ∧
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
54 | 47, 51, 53 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
∃𝑎 ∈ (𝒫
𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
55 | 54 | ex 413 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → ((𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin) → ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
56 | 39, 55 | impbid 211 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
57 | 1, 8 | syl 17 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) Fn 𝒫 𝑂) |
58 | | fvelimab 6841 |
. . . . . 6
⊢
(((𝟭‘𝑂) Fn 𝒫 𝑂 ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
59 | 57, 4, 58 | sylancl 586 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
60 | | cnveq 5782 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ◡𝑓 = ◡𝑔) |
61 | 60 | imaeq1d 5968 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (◡𝑓 “ {1}) = (◡𝑔 “ {1})) |
62 | 61 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → ((◡𝑓 “ {1}) ∈ Fin ↔ (◡𝑔 “ {1}) ∈ Fin)) |
63 | 62 | elrab 3624 |
. . . . . 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 311 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ 𝑔 ∈ {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
66 | 65 | eqrdv 2736 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) = {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |
67 | 12, 13, 66 | f1oeq123d 6710 |
. 2
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
68 | 6, 67 | mpbid 231 |
1
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |