| Step | Hyp | Ref
| Expression |
| 1 | | indf1o 32849 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)) |
| 2 | | f1of1 6847 |
. . . 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 4237 |
. . 3
⊢
(𝒫 𝑂 ∩
Fin) ⊆ 𝒫 𝑂 |
| 5 | | f1ores 6862 |
. . 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 6010 |
. . . 4
⊢
(((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) |
| 8 | | f1ofn 6849 |
. . . . . 6
⊢
((𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0,
1} ↑m 𝑂)
→ (𝟭‘𝑂)
Fn 𝒫 𝑂) |
| 9 | | fnresdm 6687 |
. . . . . 6
⊢
((𝟭‘𝑂)
Fn 𝒫 𝑂 →
((𝟭‘𝑂)
↾ 𝒫 𝑂) =
(𝟭‘𝑂)) |
| 10 | 1, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂)) |
| 11 | 10 | reseq1d 5996 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ Fin)) |
| 12 | 7, 11 | eqtr3id 2791 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) = ((𝟭‘𝑂) ↾ Fin)) |
| 13 | | eqidd 2738 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂 ∩ Fin) = (𝒫 𝑂 ∩ Fin)) |
| 14 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑂 ∈ 𝑉) |
| 15 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) |
| 16 | 4, 15 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ 𝒫 𝑂) |
| 17 | 16 | elpwid 4609 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ⊆ 𝑂) |
| 18 | | indf 32840 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
| 19 | 17, 18 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
| 20 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1}) |
| 21 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔) |
| 22 | 21 | feq1d 6720 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1} ↔ 𝑔:𝑂⟶{0, 1})) |
| 23 | 20, 22 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔:𝑂⟶{0, 1}) |
| 24 | | prex 5437 |
. . . . . . . . . . 11
⊢ {0, 1}
∈ V |
| 25 | | elmapg 8879 |
. . . . . . . . . . 11
⊢ (({0, 1}
∈ V ∧ 𝑂 ∈
𝑉) → (𝑔 ∈ ({0, 1}
↑m 𝑂)
↔ 𝑔:𝑂⟶{0, 1})) |
| 26 | 24, 25 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ↔ 𝑔:𝑂⟶{0, 1})) |
| 27 | 26 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
| 28 | 14, 23, 27 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔 ∈ ({0, 1} ↑m 𝑂)) |
| 29 | 21 | cnveqd 5886 |
. . . . . . . . . 10
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ◡((𝟭‘𝑂)‘𝑎) = ◡𝑔) |
| 30 | 29 | imaeq1d 6077 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = (◡𝑔 “ {1})) |
| 31 | | indpi1 32845 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
| 32 | 17, 31 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎) |
| 33 | | inss2 4238 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑂 ∩
Fin) ⊆ Fin |
| 34 | 33, 15 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ Fin) |
| 35 | 32, 34 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin) |
| 37 | 30, 36 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (◡𝑔 “ {1}) ∈ Fin) |
| 38 | 28, 37 | jca 511 |
. . . . . . 7
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) |
| 39 | 38 | rexlimdva2 3157 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
| 40 | | cnvimass 6100 |
. . . . . . . . . 10
⊢ (◡𝑔 “ {1}) ⊆ dom 𝑔 |
| 41 | 26 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → 𝑔:𝑂⟶{0, 1}) |
| 42 | 41 | fdmd 6746 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) → dom 𝑔 = 𝑂) |
| 43 | 42 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → dom 𝑔 = 𝑂) |
| 44 | 40, 43 | sseqtrid 4026 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ⊆ 𝑂) |
| 45 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ Fin) |
| 46 | | elfpw 9394 |
. . . . . . . . 9
⊢ ((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ↔ ((◡𝑔 “ {1}) ⊆ 𝑂 ∧ (◡𝑔 “ {1}) ∈ Fin)) |
| 47 | 44, 45, 46 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) → (◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin)) |
| 48 | | indpreima 32850 |
. . . . . . . . . . 11
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) → 𝑔 = ((𝟭‘𝑂)‘(◡𝑔 “ {1}))) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
| 50 | 41, 49 | syldan 591 |
. . . . . . . . 9
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑔 ∈ ({0, 1} ↑m 𝑂)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
| 51 | 50 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) |
| 52 | | fveqeq2 6915 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝑔 “ {1}) → (((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ ((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔)) |
| 53 | 52 | rspcev 3622 |
. . . . . . . 8
⊢ (((◡𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ∧
((𝟭‘𝑂)‘(◡𝑔 “ {1})) = 𝑔) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
| 54 | 47, 51, 53 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin)) →
∃𝑎 ∈ (𝒫
𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔) |
| 55 | 54 | ex 412 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → ((𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin) → ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
| 56 | 39, 55 | impbid 212 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ (𝑔 ∈ ({0, 1} ↑m 𝑂) ∧ (◡𝑔 “ {1}) ∈ Fin))) |
| 57 | 1, 8 | syl 17 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) Fn 𝒫 𝑂) |
| 58 | | fvelimab 6981 |
. . . . . 6
⊢
(((𝟭‘𝑂) Fn 𝒫 𝑂 ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
| 59 | 57, 4, 58 | sylancl 586 |
. . . . 5
⊢ (𝑂 ∈ 𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩
Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)) |
| 60 | | cnveq 5884 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ◡𝑓 = ◡𝑔) |
| 61 | 60 | imaeq1d 6077 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (◡𝑓 “ {1}) = (◡𝑔 “ {1})) |
| 62 | 61 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → ((◡𝑓 “ {1}) ∈ Fin ↔ (◡𝑔 “ {1}) ∈ Fin)) |
| 63 | 62 | elrab 3692 |
. . . . . 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 2735 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) = {𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |
| 67 | 12, 13, 66 | f1oeq123d 6842 |
. 2
⊢ (𝑂 ∈ 𝑉 → (((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})) |
| 68 | 6, 67 | mpbid 232 |
1
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) |