Step |
Hyp |
Ref |
Expression |
1 |
|
unit.1 |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
2 |
|
unit.2 |
⊢ 1 = ( 1r ‘ 𝑅 ) |
3 |
|
unit.3 |
⊢ ∥ = ( ∥r ‘ 𝑅 ) |
4 |
|
unit.4 |
⊢ 𝑆 = ( oppr ‘ 𝑅 ) |
5 |
|
unit.5 |
⊢ 𝐸 = ( ∥r ‘ 𝑆 ) |
6 |
|
elfvdm |
⊢ ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → 𝑅 ∈ dom Unit ) |
7 |
6 1
|
eleq2s |
⊢ ( 𝑋 ∈ 𝑈 → 𝑅 ∈ dom Unit ) |
8 |
7
|
elexd |
⊢ ( 𝑋 ∈ 𝑈 → 𝑅 ∈ V ) |
9 |
|
df-br |
⊢ ( 𝑋 ∥ 1 ↔ 〈 𝑋 , 1 〉 ∈ ∥ ) |
10 |
|
elfvdm |
⊢ ( 〈 𝑋 , 1 〉 ∈ ( ∥r ‘ 𝑅 ) → 𝑅 ∈ dom ∥r ) |
11 |
10 3
|
eleq2s |
⊢ ( 〈 𝑋 , 1 〉 ∈ ∥ → 𝑅 ∈ dom ∥r ) |
12 |
11
|
elexd |
⊢ ( 〈 𝑋 , 1 〉 ∈ ∥ → 𝑅 ∈ V ) |
13 |
9 12
|
sylbi |
⊢ ( 𝑋 ∥ 1 → 𝑅 ∈ V ) |
14 |
13
|
adantr |
⊢ ( ( 𝑋 ∥ 1 ∧ 𝑋 𝐸 1 ) → 𝑅 ∈ V ) |
15 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( ∥r ‘ 𝑟 ) = ( ∥r ‘ 𝑅 ) ) |
16 |
15 3
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( ∥r ‘ 𝑟 ) = ∥ ) |
17 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( oppr ‘ 𝑟 ) = ( oppr ‘ 𝑅 ) ) |
18 |
17 4
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( oppr ‘ 𝑟 ) = 𝑆 ) |
19 |
18
|
fveq2d |
⊢ ( 𝑟 = 𝑅 → ( ∥r ‘ ( oppr ‘ 𝑟 ) ) = ( ∥r ‘ 𝑆 ) ) |
20 |
19 5
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( ∥r ‘ ( oppr ‘ 𝑟 ) ) = 𝐸 ) |
21 |
16 20
|
ineq12d |
⊢ ( 𝑟 = 𝑅 → ( ( ∥r ‘ 𝑟 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑟 ) ) ) = ( ∥ ∩ 𝐸 ) ) |
22 |
21
|
cnveqd |
⊢ ( 𝑟 = 𝑅 → ◡ ( ( ∥r ‘ 𝑟 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑟 ) ) ) = ◡ ( ∥ ∩ 𝐸 ) ) |
23 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) ) |
24 |
23 2
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 ) |
25 |
24
|
sneqd |
⊢ ( 𝑟 = 𝑅 → { ( 1r ‘ 𝑟 ) } = { 1 } ) |
26 |
22 25
|
imaeq12d |
⊢ ( 𝑟 = 𝑅 → ( ◡ ( ( ∥r ‘ 𝑟 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑟 ) ) ) “ { ( 1r ‘ 𝑟 ) } ) = ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ) |
27 |
|
df-unit |
⊢ Unit = ( 𝑟 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑟 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑟 ) ) ) “ { ( 1r ‘ 𝑟 ) } ) ) |
28 |
3
|
fvexi |
⊢ ∥ ∈ V |
29 |
28
|
inex1 |
⊢ ( ∥ ∩ 𝐸 ) ∈ V |
30 |
29
|
cnvex |
⊢ ◡ ( ∥ ∩ 𝐸 ) ∈ V |
31 |
30
|
imaex |
⊢ ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ∈ V |
32 |
26 27 31
|
fvmpt |
⊢ ( 𝑅 ∈ V → ( Unit ‘ 𝑅 ) = ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ) |
33 |
1 32
|
eqtrid |
⊢ ( 𝑅 ∈ V → 𝑈 = ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ) |
34 |
33
|
eleq2d |
⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ) ) |
35 |
|
inss1 |
⊢ ( ∥ ∩ 𝐸 ) ⊆ ∥ |
36 |
3
|
reldvdsr |
⊢ Rel ∥ |
37 |
|
relss |
⊢ ( ( ∥ ∩ 𝐸 ) ⊆ ∥ → ( Rel ∥ → Rel ( ∥ ∩ 𝐸 ) ) ) |
38 |
35 36 37
|
mp2 |
⊢ Rel ( ∥ ∩ 𝐸 ) |
39 |
|
eliniseg2 |
⊢ ( Rel ( ∥ ∩ 𝐸 ) → ( 𝑋 ∈ ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ↔ 𝑋 ( ∥ ∩ 𝐸 ) 1 ) ) |
40 |
38 39
|
ax-mp |
⊢ ( 𝑋 ∈ ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ↔ 𝑋 ( ∥ ∩ 𝐸 ) 1 ) |
41 |
|
brin |
⊢ ( 𝑋 ( ∥ ∩ 𝐸 ) 1 ↔ ( 𝑋 ∥ 1 ∧ 𝑋 𝐸 1 ) ) |
42 |
40 41
|
bitri |
⊢ ( 𝑋 ∈ ( ◡ ( ∥ ∩ 𝐸 ) “ { 1 } ) ↔ ( 𝑋 ∥ 1 ∧ 𝑋 𝐸 1 ) ) |
43 |
34 42
|
bitrdi |
⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∥ 1 ∧ 𝑋 𝐸 1 ) ) ) |
44 |
8 14 43
|
pm5.21nii |
⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∥ 1 ∧ 𝑋 𝐸 1 ) ) |