Metamath Proof Explorer

Theorem dffun10

Description: Another potential definition of functionality. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/ . (Contributed by Scott Fenton, 30-Aug-2017)

Ref Expression
Assertion dffun10 ⊢Fun⁡F↔F⊆I∘V∖V∖I∘F

Proof

Step Hyp Ref Expression
1 impexp ⊢xy∈F∧xz∈F→y=z↔xy∈F→xz∈F→y=z
2 1 albii ⊢∀zxy∈F∧xz∈F→y=z↔∀zxy∈F→xz∈F→y=z
3 19.21v ⊢∀zxy∈F→xz∈F→y=z↔xy∈F→∀zxz∈F→y=z
4 vex ⊢x∈V
5 vex ⊢y∈V
6 4 5 opelco ⊢xy∈V∖I∘F↔∃zxFz∧zV∖Iy
7 df-br ⊢xFz↔xz∈F
8 brv ⊢zVy
9 brdif ⊢zV∖Iy↔zVy∧¬zIy
10 8 9 mpbiran ⊢zV∖Iy↔¬zIy
11 5 ideq ⊢zIy↔z=y
12 equcom ⊢z=y↔y=z
13 11 12 bitri ⊢zIy↔y=z
14 10 13 xchbinx ⊢zV∖Iy↔¬y=z
15 7 14 anbi12i ⊢xFz∧zV∖Iy↔xz∈F∧¬y=z
16 15 exbii ⊢∃zxFz∧zV∖Iy↔∃zxz∈F∧¬y=z
17 exanali ⊢∃zxz∈F∧¬y=z↔¬∀zxz∈F→y=z
18 6 16 17 3bitri ⊢xy∈V∖I∘F↔¬∀zxz∈F→y=z
19 18 con2bii ⊢∀zxz∈F→y=z↔¬xy∈V∖I∘F
20 opex ⊢xy∈V
21 eldif ⊢xy∈V∖V∖I∘F↔xy∈V∧¬xy∈V∖I∘F
22 20 21 mpbiran ⊢xy∈V∖V∖I∘F↔¬xy∈V∖I∘F
23 19 22 bitr4i ⊢∀zxz∈F→y=z↔xy∈V∖V∖I∘F
24 23 imbi2i ⊢xy∈F→∀zxz∈F→y=z↔xy∈F→xy∈V∖V∖I∘F
25 2 3 24 3bitri ⊢∀zxy∈F∧xz∈F→y=z↔xy∈F→xy∈V∖V∖I∘F
26 25 2albii ⊢∀x∀y∀zxy∈F∧xz∈F→y=z↔∀x∀yxy∈F→xy∈V∖V∖I∘F
27 ssrel ⊢Rel⁡F→F⊆V∖V∖I∘F↔∀x∀yxy∈F→xy∈V∖V∖I∘F
28 26 27 bitr4id ⊢Rel⁡F→∀x∀y∀zxy∈F∧xz∈F→y=z↔F⊆V∖V∖I∘F
29 28 pm5.32i ⊢Rel⁡F∧∀x∀y∀zxy∈F∧xz∈F→y=z↔Rel⁡F∧F⊆V∖V∖I∘F
30 dffun4 ⊢Fun⁡F↔Rel⁡F∧∀x∀y∀zxy∈F∧xz∈F→y=z
31 sscoid ⊢F⊆I∘V∖V∖I∘F↔Rel⁡F∧F⊆V∖V∖I∘F
32 29 30 31 3bitr4i ⊢Fun⁡F↔F⊆I∘V∖V∖I∘F