Step | Hyp | Ref
| Expression |
1 | | elfvdm 6130 |
. . . 4
⊢ (𝑋 ∈ (Unit‘𝑅) → 𝑅 ∈ dom Unit) |
2 | | unit.1 |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
3 | 1, 2 | eleq2s 2706 |
. . 3
⊢ (𝑋 ∈ 𝑈 → 𝑅 ∈ dom Unit) |
4 | 3 | elexd 3187 |
. 2
⊢ (𝑋 ∈ 𝑈 → 𝑅 ∈ V) |
5 | | df-br 4584 |
. . . 4
⊢ (𝑋 ∥ 1 ↔ 〈𝑋, 1 〉 ∈ ∥
) |
6 | | elfvdm 6130 |
. . . . . 6
⊢
(〈𝑋, 1 〉 ∈
(∥r‘𝑅) → 𝑅 ∈ dom
∥r) |
7 | | unit.3 |
. . . . . 6
⊢ ∥ =
(∥r‘𝑅) |
8 | 6, 7 | eleq2s 2706 |
. . . . 5
⊢
(〈𝑋, 1 〉 ∈
∥
→ 𝑅 ∈ dom
∥r) |
9 | 8 | elexd 3187 |
. . . 4
⊢
(〈𝑋, 1 〉 ∈
∥
→ 𝑅 ∈
V) |
10 | 5, 9 | sylbi 206 |
. . 3
⊢ (𝑋 ∥ 1 → 𝑅 ∈ V) |
11 | 10 | adantr 480 |
. 2
⊢ ((𝑋 ∥ 1 ∧ 𝑋𝐸 1 ) → 𝑅 ∈ V) |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(∥r‘𝑟) = (∥r‘𝑅)) |
13 | 12, 7 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(∥r‘𝑟) = ∥ ) |
14 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (oppr‘𝑟) =
(oppr‘𝑅)) |
15 | | unit.4 |
. . . . . . . . . . . 12
⊢ 𝑆 =
(oppr‘𝑅) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (oppr‘𝑟) = 𝑆) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(∥r‘(oppr‘𝑟)) =
(∥r‘𝑆)) |
18 | | unit.5 |
. . . . . . . . . 10
⊢ 𝐸 =
(∥r‘𝑆) |
19 | 17, 18 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(∥r‘(oppr‘𝑟)) = 𝐸) |
20 | 13, 19 | ineq12d 3777 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ( ∥ ∩ 𝐸)) |
21 | 20 | cnveqd 5220 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ◡( ∥ ∩ 𝐸)) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
23 | | unit.2 |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
25 | 24 | sneqd 4137 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → {(1r‘𝑟)} = { 1 }) |
26 | 21, 25 | imaeq12d 5386 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “
{(1r‘𝑟)})
= (◡( ∥ ∩ 𝐸) “ { 1 })) |
27 | | df-unit 18465 |
. . . . . 6
⊢ Unit =
(𝑟 ∈ V ↦ (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “
{(1r‘𝑟)})) |
28 | | fvex 6113 |
. . . . . . . . . 10
⊢
(∥r‘𝑅) ∈ V |
29 | 7, 28 | eqeltri 2684 |
. . . . . . . . 9
⊢ ∥ ∈
V |
30 | 29 | inex1 4727 |
. . . . . . . 8
⊢ ( ∥ ∩
𝐸) ∈
V |
31 | 30 | cnvex 7006 |
. . . . . . 7
⊢ ◡( ∥ ∩ 𝐸) ∈ V |
32 | 31 | imaex 6996 |
. . . . . 6
⊢ (◡( ∥ ∩ 𝐸) “ { 1 }) ∈
V |
33 | 26, 27, 32 | fvmpt 6191 |
. . . . 5
⊢ (𝑅 ∈ V →
(Unit‘𝑅) = (◡( ∥ ∩ 𝐸) “ { 1 })) |
34 | 2, 33 | syl5eq 2656 |
. . . 4
⊢ (𝑅 ∈ V → 𝑈 = (◡( ∥ ∩ 𝐸) “ { 1 })) |
35 | 34 | eleq2d 2673 |
. . 3
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }))) |
36 | | inss1 3795 |
. . . . . 6
⊢ ( ∥ ∩
𝐸) ⊆ ∥ |
37 | 7 | reldvdsr 18467 |
. . . . . 6
⊢ Rel ∥ |
38 | | relss 5129 |
. . . . . 6
⊢ (( ∥ ∩
𝐸) ⊆ ∥ →
(Rel ∥ → Rel ( ∥ ∩
𝐸))) |
39 | 36, 37, 38 | mp2 9 |
. . . . 5
⊢ Rel (
∥
∩ 𝐸) |
40 | | eliniseg2 5424 |
. . . . 5
⊢ (Rel (
∥
∩ 𝐸) → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 )) |
41 | 39, 40 | ax-mp 5 |
. . . 4
⊢ (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 ) |
42 | | brin 4634 |
. . . 4
⊢ (𝑋( ∥ ∩ 𝐸) 1 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |
43 | 41, 42 | bitri 263 |
. . 3
⊢ (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |
44 | 35, 43 | syl6bb 275 |
. 2
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 ))) |
45 | 4, 11, 44 | pm5.21nii 367 |
1
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |