Proof of Theorem dom2lem
Step | Hyp | Ref
| Expression |
1 | | dom2d.1 |
. . . 4
⊢ (φ → (x ∈ A → 𝐶 ∈
B)) |
2 | 1 | ralrimiv 2385 |
. . 3
⊢ (φ → ∀x ∈ A 𝐶 ∈ B) |
3 | | eqid 2037 |
. . . 4
⊢ (x ∈ A ↦ 𝐶) = (x
∈ A
↦ 𝐶) |
4 | 3 | fmpt 5262 |
. . 3
⊢ (∀x ∈ A 𝐶 ∈ B ↔
(x ∈
A ↦ 𝐶):A⟶B) |
5 | 2, 4 | sylib 127 |
. 2
⊢ (φ → (x ∈ A ↦ 𝐶):A⟶B) |
6 | 1 | imp 115 |
. . . . . . 7
⊢ ((φ ∧ x ∈ A) → 𝐶 ∈
B) |
7 | 3 | fvmpt2 5197 |
. . . . . . . 8
⊢
((x ∈ A ∧ 𝐶 ∈
B) → ((x ∈ A ↦ 𝐶)‘x) = 𝐶) |
8 | 7 | adantll 445 |
. . . . . . 7
⊢ (((φ ∧ x ∈ A) ∧ 𝐶 ∈ B) →
((x ∈
A ↦ 𝐶)‘x) = 𝐶) |
9 | 6, 8 | mpdan 398 |
. . . . . 6
⊢ ((φ ∧ x ∈ A) → ((x
∈ A
↦ 𝐶)‘x) = 𝐶) |
10 | 9 | adantrr 448 |
. . . . 5
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → ((x ∈ A ↦ 𝐶)‘x) = 𝐶) |
11 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎx(φ ∧ y ∈ A) |
12 | | nffvmpt1 5129 |
. . . . . . . . 9
⊢
Ⅎx((x ∈ A ↦ 𝐶)‘y) |
13 | 12 | nfeq1 2184 |
. . . . . . . 8
⊢
Ⅎx((x ∈ A ↦ 𝐶)‘y) = 𝐷 |
14 | 11, 13 | nfim 1461 |
. . . . . . 7
⊢
Ⅎx((φ ∧ y ∈ A) → ((x
∈ A
↦ 𝐶)‘y) = 𝐷) |
15 | | eleq1 2097 |
. . . . . . . . . 10
⊢ (x = y →
(x ∈
A ↔ y ∈ A)) |
16 | 15 | anbi2d 437 |
. . . . . . . . 9
⊢ (x = y →
((φ ∧
x ∈
A) ↔ (φ ∧ y ∈ A))) |
17 | 16 | imbi1d 220 |
. . . . . . . 8
⊢ (x = y →
(((φ ∧
x ∈
A) → ((x ∈ A ↦ 𝐶)‘x) = 𝐶) ↔ ((φ ∧ y ∈ A) → ((x
∈ A
↦ 𝐶)‘x) = 𝐶))) |
18 | 15 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (x = y →
((x ∈
A ∧
y ∈
A) ↔ (y ∈ A ∧ y ∈ A))) |
19 | | anidm 376 |
. . . . . . . . . . . 12
⊢
((y ∈ A ∧ y ∈ A) ↔
y ∈
A) |
20 | 18, 19 | syl6bb 185 |
. . . . . . . . . . 11
⊢ (x = y →
((x ∈
A ∧
y ∈
A) ↔ y ∈ A)) |
21 | 20 | anbi2d 437 |
. . . . . . . . . 10
⊢ (x = y →
((φ ∧
(x ∈
A ∧
y ∈
A)) ↔ (φ ∧ y ∈ A))) |
22 | | fveq2 5121 |
. . . . . . . . . . . . 13
⊢ (x = y →
((x ∈
A ↦ 𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y)) |
23 | 22 | adantr 261 |
. . . . . . . . . . . 12
⊢
((x = y ∧ (φ ∧
(x ∈
A ∧
y ∈
A))) → ((x ∈ A ↦ 𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y)) |
24 | | dom2d.2 |
. . . . . . . . . . . . . 14
⊢ (φ → ((x ∈ A ∧ y ∈ A) → (𝐶 = 𝐷 ↔ x = y))) |
25 | 24 | imp 115 |
. . . . . . . . . . . . 13
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → (𝐶 = 𝐷 ↔ x = y)) |
26 | 25 | biimparc 283 |
. . . . . . . . . . . 12
⊢
((x = y ∧ (φ ∧
(x ∈
A ∧
y ∈
A))) → 𝐶 = 𝐷) |
27 | 23, 26 | eqeq12d 2051 |
. . . . . . . . . . 11
⊢
((x = y ∧ (φ ∧
(x ∈
A ∧
y ∈
A))) → (((x ∈ A ↦ 𝐶)‘x) = 𝐶 ↔ ((x ∈ A ↦ 𝐶)‘y) = 𝐷)) |
28 | 27 | ex 108 |
. . . . . . . . . 10
⊢ (x = y →
((φ ∧
(x ∈
A ∧
y ∈
A)) → (((x ∈ A ↦ 𝐶)‘x) = 𝐶 ↔ ((x ∈ A ↦ 𝐶)‘y) = 𝐷))) |
29 | 21, 28 | sylbird 159 |
. . . . . . . . 9
⊢ (x = y →
((φ ∧
y ∈
A) → (((x ∈ A ↦ 𝐶)‘x) = 𝐶 ↔ ((x ∈ A ↦ 𝐶)‘y) = 𝐷))) |
30 | 29 | pm5.74d 171 |
. . . . . . . 8
⊢ (x = y →
(((φ ∧
y ∈
A) → ((x ∈ A ↦ 𝐶)‘x) = 𝐶) ↔ ((φ ∧ y ∈ A) → ((x
∈ A
↦ 𝐶)‘y) = 𝐷))) |
31 | 17, 30 | bitrd 177 |
. . . . . . 7
⊢ (x = y →
(((φ ∧
x ∈
A) → ((x ∈ A ↦ 𝐶)‘x) = 𝐶) ↔ ((φ ∧ y ∈ A) → ((x
∈ A
↦ 𝐶)‘y) = 𝐷))) |
32 | 14, 31, 9 | chvar 1637 |
. . . . . 6
⊢ ((φ ∧ y ∈ A) → ((x
∈ A
↦ 𝐶)‘y) = 𝐷) |
33 | 32 | adantrl 447 |
. . . . 5
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → ((x ∈ A ↦ 𝐶)‘y) = 𝐷) |
34 | 10, 33 | eqeq12d 2051 |
. . . 4
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → (((x ∈ A ↦ 𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y) ↔ 𝐶 = 𝐷)) |
35 | 25 | biimpd 132 |
. . . 4
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → (𝐶 = 𝐷 → x = y)) |
36 | 34, 35 | sylbid 139 |
. . 3
⊢ ((φ ∧
(x ∈
A ∧
y ∈
A)) → (((x ∈ A ↦ 𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y) → x =
y)) |
37 | 36 | ralrimivva 2395 |
. 2
⊢ (φ → ∀x ∈ A ∀y ∈ A (((x ∈ A ↦ 𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y) → x =
y)) |
38 | | nfmpt1 3841 |
. . 3
⊢
Ⅎx(x ∈ A ↦ 𝐶) |
39 | | nfcv 2175 |
. . 3
⊢
Ⅎy(x ∈ A ↦ 𝐶) |
40 | 38, 39 | dff13f 5352 |
. 2
⊢
((x ∈ A ↦
𝐶):A–1-1→B ↔
((x ∈
A ↦ 𝐶):A⟶B ∧ ∀x ∈ A ∀y ∈ A (((x ∈ A ↦
𝐶)‘x) = ((x ∈ A ↦
𝐶)‘y) → x =
y))) |
41 | 5, 37, 40 | sylanbrc 394 |
1
⊢ (φ → (x ∈ A ↦ 𝐶):A–1-1→B) |