Step | Hyp | Ref
| Expression |
1 | | ffn 5958 |
. . 3
⊢ (𝐹:𝑂⟶{0, 1} → 𝐹 Fn 𝑂) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 Fn 𝑂) |
3 | | cnvimass 5404 |
. . . . 5
⊢ (◡𝐹 “ {1}) ⊆ dom 𝐹 |
4 | | fdm 5964 |
. . . . . 6
⊢ (𝐹:𝑂⟶{0, 1} → dom 𝐹 = 𝑂) |
5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → dom 𝐹 = 𝑂) |
6 | 3, 5 | syl5sseq 3616 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (◡𝐹 “ {1}) ⊆ 𝑂) |
7 | | indf 29405 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂) → ((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
8 | 6, 7 | syldan 486 |
. . 3
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
9 | | ffn 5958 |
. . 3
⊢
(((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1} →
((𝟭‘𝑂)‘(◡𝐹 “ {1})) Fn 𝑂) |
10 | 8, 9 | syl 17 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})) Fn 𝑂) |
11 | | simpr 476 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹:𝑂⟶{0, 1}) |
12 | 11 | ffvelrnda 6267 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {0, 1}) |
13 | | prcom 4211 |
. . . 4
⊢ {0, 1} =
{1, 0} |
14 | 12, 13 | syl6eleq 2698 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {1, 0}) |
15 | 8 | ffvelrnda 6267 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {0, 1}) |
16 | 15, 13 | syl6eleq 2698 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {1, 0}) |
17 | | simpll 786 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑂 ∈ 𝑉) |
18 | 6 | adantr 480 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (◡𝐹 “ {1}) ⊆ 𝑂) |
19 | | simpr 476 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑥 ∈ 𝑂) |
20 | | ind1a 29410 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
21 | 17, 18, 19, 20 | syl3anc 1318 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
22 | | fniniseg 6246 |
. . . . . 6
⊢ (𝐹 Fn 𝑂 → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
23 | 2, 22 | syl 17 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
24 | 23 | baibd 946 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝐹‘𝑥) = 1)) |
25 | 21, 24 | bitr2d 268 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((𝐹‘𝑥) = 1 ↔ (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1)) |
26 | 14, 16, 25 | elpreq 28744 |
. 2
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) = (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥)) |
27 | 2, 10, 26 | eqfnfvd 6222 |
1
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) |