Step | Hyp | Ref
| Expression |
1 | | ffn 6545 |
. . 3
⊢ (𝐹:𝑂⟶{0, 1} → 𝐹 Fn 𝑂) |
2 | 1 | adantl 485 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 Fn 𝑂) |
3 | | cnvimass 5949 |
. . . . 5
⊢ (◡𝐹 “ {1}) ⊆ dom 𝐹 |
4 | | fdm 6554 |
. . . . . 6
⊢ (𝐹:𝑂⟶{0, 1} → dom 𝐹 = 𝑂) |
5 | 4 | adantl 485 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → dom 𝐹 = 𝑂) |
6 | 3, 5 | sseqtrid 3953 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (◡𝐹 “ {1}) ⊆ 𝑂) |
7 | | indf 31695 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂) → ((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
8 | 6, 7 | syldan 594 |
. . 3
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
9 | 8 | ffnd 6546 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})) Fn 𝑂) |
10 | | simpr 488 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹:𝑂⟶{0, 1}) |
11 | 10 | ffvelrnda 6904 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {0, 1}) |
12 | | prcom 4648 |
. . . 4
⊢ {0, 1} =
{1, 0} |
13 | 11, 12 | eleqtrdi 2848 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {1, 0}) |
14 | 8 | ffvelrnda 6904 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {0, 1}) |
15 | 14, 12 | eleqtrdi 2848 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {1, 0}) |
16 | | simpll 767 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑂 ∈ 𝑉) |
17 | 6 | adantr 484 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (◡𝐹 “ {1}) ⊆ 𝑂) |
18 | | simpr 488 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑥 ∈ 𝑂) |
19 | | ind1a 31699 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
20 | 16, 17, 18, 19 | syl3anc 1373 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
21 | | fniniseg 6880 |
. . . . . 6
⊢ (𝐹 Fn 𝑂 → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
22 | 2, 21 | syl 17 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
23 | 22 | baibd 543 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝐹‘𝑥) = 1)) |
24 | 20, 23 | bitr2d 283 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((𝐹‘𝑥) = 1 ↔ (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1)) |
25 | 13, 15, 24 | elpreq 30597 |
. 2
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) = (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥)) |
26 | 2, 9, 25 | eqfnfvd 6855 |
1
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) |