Proof of Theorem elovmporab
Step | Hyp | Ref
| Expression |
1 | | elovmporab.o |
. . 3
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ 𝑀 ∣ 𝜑}) |
2 | 1 | elmpocl 7489 |
. 2
⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
3 | 1 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ 𝑀 ∣ 𝜑})) |
4 | | sbceq1a 3722 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (𝜑 ↔ [𝑌 / 𝑦]𝜑)) |
5 | | sbceq1a 3722 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ([𝑌 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)) |
6 | 4, 5 | sylan9bbr 510 |
. . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ (((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)) |
8 | 7 | rabbidv 3404 |
. . . . 5
⊢ (((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → {𝑧 ∈ 𝑀 ∣ 𝜑} = {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑}) |
9 | | eqidd 2739 |
. . . . 5
⊢ (((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑥 = 𝑋) → V = V) |
10 | | simpl 482 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑋 ∈ V) |
11 | | simpr 484 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑌 ∈ V) |
12 | | elovmporab.v |
. . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑀 ∈ V) |
13 | | rabexg 5250 |
. . . . . 6
⊢ (𝑀 ∈ V → {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} ∈ V) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} ∈ V) |
15 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥𝑋 |
16 | 15 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑥 𝑋 ∈ V |
17 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑥𝑌 |
18 | 17 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑥 𝑌 ∈ V |
19 | 16, 18 | nfan 1903 |
. . . . 5
⊢
Ⅎ𝑥(𝑋 ∈ V ∧ 𝑌 ∈ V) |
20 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑦𝑋 |
21 | 20 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑦 𝑋 ∈ V |
22 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑦𝑌 |
23 | 22 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑦 𝑌 ∈ V |
24 | 21, 23 | nfan 1903 |
. . . . 5
⊢
Ⅎ𝑦(𝑋 ∈ V ∧ 𝑌 ∈ V) |
25 | | nfsbc1v 3731 |
. . . . . 6
⊢
Ⅎ𝑥[𝑋 / 𝑥][𝑌 / 𝑦]𝜑 |
26 | | nfcv 2906 |
. . . . . 6
⊢
Ⅎ𝑥𝑀 |
27 | 25, 26 | nfrabw 3311 |
. . . . 5
⊢
Ⅎ𝑥{𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} |
28 | | nfsbc1v 3731 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑌 / 𝑦]𝜑 |
29 | 20, 28 | nfsbcw 3733 |
. . . . . 6
⊢
Ⅎ𝑦[𝑋 / 𝑥][𝑌 / 𝑦]𝜑 |
30 | | nfcv 2906 |
. . . . . 6
⊢
Ⅎ𝑦𝑀 |
31 | 29, 30 | nfrabw 3311 |
. . . . 5
⊢
Ⅎ𝑦{𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} |
32 | 3, 8, 9, 10, 11, 14, 19, 24, 20, 17, 27, 31 | ovmpodxf 7401 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋𝑂𝑌) = {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑}) |
33 | 32 | eleq2d 2824 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑍 ∈ (𝑋𝑂𝑌) ↔ 𝑍 ∈ {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑})) |
34 | | df-3an 1087 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀) ↔ ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑍 ∈ 𝑀)) |
35 | 34 | simplbi2com 502 |
. . . 4
⊢ (𝑍 ∈ 𝑀 → ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀))) |
36 | | elrabi 3611 |
. . . 4
⊢ (𝑍 ∈ {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} → 𝑍 ∈ 𝑀) |
37 | 35, 36 | syl11 33 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑍 ∈ {𝑧 ∈ 𝑀 ∣ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑} → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀))) |
38 | 33, 37 | sylbid 239 |
. 2
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀))) |
39 | 2, 38 | mpcom 38 |
1
⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀)) |