| Step | Hyp | Ref
| Expression |
| 1 | | ffn 6736 |
. . 3
⊢ (𝐹:𝑂⟶{0, 1} → 𝐹 Fn 𝑂) |
| 2 | 1 | adantl 481 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 Fn 𝑂) |
| 3 | | cnvimass 6100 |
. . . . 5
⊢ (◡𝐹 “ {1}) ⊆ dom 𝐹 |
| 4 | | fdm 6745 |
. . . . . 6
⊢ (𝐹:𝑂⟶{0, 1} → dom 𝐹 = 𝑂) |
| 5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → dom 𝐹 = 𝑂) |
| 6 | 3, 5 | sseqtrid 4026 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (◡𝐹 “ {1}) ⊆ 𝑂) |
| 7 | | indf 32840 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂) → ((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
| 8 | 6, 7 | syldan 591 |
. . 3
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})):𝑂⟶{0, 1}) |
| 9 | 8 | ffnd 6737 |
. 2
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) →
((𝟭‘𝑂)‘(◡𝐹 “ {1})) Fn 𝑂) |
| 10 | | simpr 484 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹:𝑂⟶{0, 1}) |
| 11 | 10 | ffvelcdmda 7104 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {0, 1}) |
| 12 | | prcom 4732 |
. . . 4
⊢ {0, 1} =
{1, 0} |
| 13 | 11, 12 | eleqtrdi 2851 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) ∈ {1, 0}) |
| 14 | 8 | ffvelcdmda 7104 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {0, 1}) |
| 15 | 14, 12 | eleqtrdi 2851 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) ∈ {1, 0}) |
| 16 | | simpll 767 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑂 ∈ 𝑉) |
| 17 | 6 | adantr 480 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (◡𝐹 “ {1}) ⊆ 𝑂) |
| 18 | | simpr 484 |
. . . . 5
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → 𝑥 ∈ 𝑂) |
| 19 | | ind1a 32844 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ (◡𝐹 “ {1}) ⊆ 𝑂 ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
| 20 | 16, 17, 18, 19 | syl3anc 1373 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1 ↔ 𝑥 ∈ (◡𝐹 “ {1}))) |
| 21 | | fniniseg 7080 |
. . . . . 6
⊢ (𝐹 Fn 𝑂 → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
| 22 | 2, 21 | syl 17 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝑥 ∈ 𝑂 ∧ (𝐹‘𝑥) = 1))) |
| 23 | 22 | baibd 539 |
. . . 4
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝑥 ∈ (◡𝐹 “ {1}) ↔ (𝐹‘𝑥) = 1)) |
| 24 | 20, 23 | bitr2d 280 |
. . 3
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → ((𝐹‘𝑥) = 1 ↔ (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥) = 1)) |
| 25 | 13, 15, 24 | elpreq 32548 |
. 2
⊢ (((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) ∧ 𝑥 ∈ 𝑂) → (𝐹‘𝑥) = (((𝟭‘𝑂)‘(◡𝐹 “ {1}))‘𝑥)) |
| 26 | 2, 9, 25 | eqfnfvd 7054 |
1
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) |