Description: Reverse closure for an operation value, analogous to afvvv . In contrast to ovrcl , elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | aovprc.1 | ⊢ Rel dom 𝐹 | |
| Assertion | aovrcl | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aovprc.1 | ⊢ Rel dom 𝐹 | |
| 2 | df-aov | ⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) | |
| 3 | 2 | eleq1i | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 ↔ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝐶 ) |
| 4 | afvvdm | ⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) | |
| 5 | df-br | ⊢ ( 𝐴 dom 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) | |
| 6 | 1 | brrelex12i | ⊢ ( 𝐴 dom 𝐹 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 7 | 5 6 | sylbir | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 8 | 4 7 | syl | ⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝐶 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 9 | 3 8 | sylbi | ⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |