Step | Hyp | Ref
| Expression |
1 | | elfvdm 6480 |
. . . 4
⊢ (𝑋 ∈ (Unit‘𝑅) → 𝑅 ∈ dom Unit) |
2 | | unit.1 |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
3 | 1, 2 | eleq2s 2877 |
. . 3
⊢ (𝑋 ∈ 𝑈 → 𝑅 ∈ dom Unit) |
4 | 3 | elexd 3416 |
. 2
⊢ (𝑋 ∈ 𝑈 → 𝑅 ∈ V) |
5 | | df-br 4889 |
. . . 4
⊢ (𝑋 ∥ 1 ↔ 〈𝑋, 1 〉 ∈ ∥
) |
6 | | elfvdm 6480 |
. . . . . 6
⊢
(〈𝑋, 1 〉 ∈
(∥r‘𝑅) → 𝑅 ∈ dom
∥r) |
7 | | unit.3 |
. . . . . 6
⊢ ∥ =
(∥r‘𝑅) |
8 | 6, 7 | eleq2s 2877 |
. . . . 5
⊢
(〈𝑋, 1 〉 ∈
∥
→ 𝑅 ∈ dom
∥r) |
9 | 8 | elexd 3416 |
. . . 4
⊢
(〈𝑋, 1 〉 ∈
∥
→ 𝑅 ∈
V) |
10 | 5, 9 | sylbi 209 |
. . 3
⊢ (𝑋 ∥ 1 → 𝑅 ∈ V) |
11 | 10 | adantr 474 |
. 2
⊢ ((𝑋 ∥ 1 ∧ 𝑋𝐸 1 ) → 𝑅 ∈ V) |
12 | | fveq2 6448 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(∥r‘𝑟) = (∥r‘𝑅)) |
13 | 12, 7 | syl6eqr 2832 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(∥r‘𝑟) = ∥ ) |
14 | | fveq2 6448 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (oppr‘𝑟) =
(oppr‘𝑅)) |
15 | | unit.4 |
. . . . . . . . . . . 12
⊢ 𝑆 =
(oppr‘𝑅) |
16 | 14, 15 | syl6eqr 2832 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (oppr‘𝑟) = 𝑆) |
17 | 16 | fveq2d 6452 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(∥r‘(oppr‘𝑟)) =
(∥r‘𝑆)) |
18 | | unit.5 |
. . . . . . . . . 10
⊢ 𝐸 =
(∥r‘𝑆) |
19 | 17, 18 | syl6eqr 2832 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(∥r‘(oppr‘𝑟)) = 𝐸) |
20 | 13, 19 | ineq12d 4038 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ( ∥ ∩ 𝐸)) |
21 | 20 | cnveqd 5545 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ◡( ∥ ∩ 𝐸)) |
22 | | fveq2 6448 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
23 | | unit.2 |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
24 | 22, 23 | syl6eqr 2832 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
25 | 24 | sneqd 4410 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → {(1r‘𝑟)} = { 1 }) |
26 | 21, 25 | imaeq12d 5723 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “
{(1r‘𝑟)})
= (◡( ∥ ∩ 𝐸) “ { 1 })) |
27 | | df-unit 19040 |
. . . . . 6
⊢ Unit =
(𝑟 ∈ V ↦ (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “
{(1r‘𝑟)})) |
28 | 7 | fvexi 6462 |
. . . . . . . . 9
⊢ ∥ ∈
V |
29 | 28 | inex1 5038 |
. . . . . . . 8
⊢ ( ∥ ∩
𝐸) ∈
V |
30 | 29 | cnvex 7394 |
. . . . . . 7
⊢ ◡( ∥ ∩ 𝐸) ∈ V |
31 | 30 | imaex 7385 |
. . . . . 6
⊢ (◡( ∥ ∩ 𝐸) “ { 1 }) ∈
V |
32 | 26, 27, 31 | fvmpt 6544 |
. . . . 5
⊢ (𝑅 ∈ V →
(Unit‘𝑅) = (◡( ∥ ∩ 𝐸) “ { 1 })) |
33 | 2, 32 | syl5eq 2826 |
. . . 4
⊢ (𝑅 ∈ V → 𝑈 = (◡( ∥ ∩ 𝐸) “ { 1 })) |
34 | 33 | eleq2d 2845 |
. . 3
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }))) |
35 | | inss1 4053 |
. . . . . 6
⊢ ( ∥ ∩
𝐸) ⊆ ∥ |
36 | 7 | reldvdsr 19042 |
. . . . . 6
⊢ Rel ∥ |
37 | | relss 5456 |
. . . . . 6
⊢ (( ∥ ∩
𝐸) ⊆ ∥ →
(Rel ∥ → Rel ( ∥ ∩
𝐸))) |
38 | 35, 36, 37 | mp2 9 |
. . . . 5
⊢ Rel (
∥
∩ 𝐸) |
39 | | eliniseg2 5761 |
. . . . 5
⊢ (Rel (
∥
∩ 𝐸) → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 )) |
40 | 38, 39 | ax-mp 5 |
. . . 4
⊢ (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 ) |
41 | | brin 4940 |
. . . 4
⊢ (𝑋( ∥ ∩ 𝐸) 1 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |
42 | 40, 41 | bitri 267 |
. . 3
⊢ (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |
43 | 34, 42 | syl6bb 279 |
. 2
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 ))) |
44 | 4, 11, 43 | pm5.21nii 370 |
1
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |