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