Proof of Theorem elfvmptrab1
Step | Hyp | Ref
| Expression |
1 | | ne0i 3880 |
. . 3
⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝐹‘𝑋) ≠ ∅) |
2 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝑋 ∈ dom 𝐹 → (𝐹‘𝑋) = ∅) |
3 | 2 | necon1ai 2809 |
. . 3
⊢ ((𝐹‘𝑋) ≠ ∅ → 𝑋 ∈ dom 𝐹) |
4 | | elfvmptrab1.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) |
5 | 4 | dmmptss 5548 |
. . . . . . 7
⊢ dom 𝐹 ⊆ 𝑉 |
6 | 5 | sseli 3564 |
. . . . . 6
⊢ (𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝑉) |
7 | | elfvmptrab1.v |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) |
8 | | rabexg 4739 |
. . . . . . 7
⊢
(⦋𝑋 /
𝑚⦌𝑀 ∈ V → {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} ∈ V) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . 6
⊢ (𝑋 ∈ dom 𝐹 → {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} ∈ V) |
10 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑋 |
11 | | nfsbc1v 3422 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑋 / 𝑥]𝜑 |
12 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑀 |
13 | 10, 12 | nfcsb 3517 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑋 / 𝑚⦌𝑀 |
14 | 11, 13 | nfrab 3100 |
. . . . . . 7
⊢
Ⅎ𝑥{𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} |
15 | | csbeq1 3502 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ⦋𝑥 / 𝑚⦌𝑀 = ⦋𝑋 / 𝑚⦌𝑀) |
16 | | sbceq1a 3413 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝜑 ↔ [𝑋 / 𝑥]𝜑)) |
17 | 15, 16 | rabeqbidv 3168 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑} = {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑}) |
18 | 10, 14, 17, 4 | fvmptf 6209 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} ∈ V) → (𝐹‘𝑋) = {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑}) |
19 | 6, 9, 18 | syl2anc 691 |
. . . . 5
⊢ (𝑋 ∈ dom 𝐹 → (𝐹‘𝑋) = {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑}) |
20 | 19 | eleq2d 2673 |
. . . 4
⊢ (𝑋 ∈ dom 𝐹 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑})) |
21 | | elrabi 3328 |
. . . . . 6
⊢ (𝑌 ∈ {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} → 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀) |
22 | 6, 21 | anim12i 588 |
. . . . 5
⊢ ((𝑋 ∈ dom 𝐹 ∧ 𝑌 ∈ {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑}) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) |
23 | 22 | ex 449 |
. . . 4
⊢ (𝑋 ∈ dom 𝐹 → (𝑌 ∈ {𝑦 ∈ ⦋𝑋 / 𝑚⦌𝑀 ∣ [𝑋 / 𝑥]𝜑} → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))) |
24 | 20, 23 | sylbid 229 |
. . 3
⊢ (𝑋 ∈ dom 𝐹 → (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))) |
25 | 1, 3, 24 | 3syl 18 |
. 2
⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))) |
26 | 25 | pm2.43i 50 |
1
⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) |