This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ↔ 𝐹 ⊆ ( I ∘ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 impexp ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ) )
2 1 albii ⊢ ( ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑧 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ) )
3 19.21v ⊢ ( ∀ 𝑧 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ) )
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑦 ∈ V
6 4 5 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V ∖ I ) ∘ 𝐹 ) ↔ ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( V ∖ I ) 𝑦 ) )
7 df-br ⊢ ( 𝑥 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 )
8 brv ⊢ 𝑧 V 𝑦
9 brdif ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ( 𝑧 V 𝑦 ∧ ¬ 𝑧 I 𝑦 ) )
10 8 9 mpbiran ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ¬ 𝑧 I 𝑦 )
11 5 ideq ⊢ ( 𝑧 I 𝑦 ↔ 𝑧 = 𝑦 )
12 equcom ⊢ ( 𝑧 = 𝑦 ↔ 𝑦 = 𝑧 )
13 11 12 bitri ⊢ ( 𝑧 I 𝑦 ↔ 𝑦 = 𝑧 )
14 10 13 xchbinx ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ¬ 𝑦 = 𝑧 )
15 7 14 anbi12i ⊢ ( ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( V ∖ I ) 𝑦 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∧ ¬ 𝑦 = 𝑧 ) )
16 15 exbii ⊢ ( ∃ 𝑧 ( 𝑥 𝐹 𝑧 ∧ 𝑧 ( V ∖ I ) 𝑦 ) ↔ ∃ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∧ ¬ 𝑦 = 𝑧 ) )
17 exanali ⊢ ( ∃ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∧ ¬ 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) )
18 6 16 17 3bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V ∖ I ) ∘ 𝐹 ) ↔ ¬ ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) )
19 18 con2bii ⊢ ( ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ↔ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V ∖ I ) ∘ 𝐹 ) )
20 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
21 eldif ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ V ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V ∖ I ) ∘ 𝐹 ) ) )
22 20 21 mpbiran ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ↔ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V ∖ I ) ∘ 𝐹 ) )
23 19 22 bitr4i ⊢ ( ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) )
24 23 imbi2i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑦 = 𝑧 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
25 2 3 24 3bitri ⊢ ( ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
26 25 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
27 ssrel ⊢ ( Rel 𝐹 → ( 𝐹 ⊆ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) ) )
28 26 27 bitr4id ⊢ ( Rel 𝐹 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ 𝐹 ⊆ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
29 28 pm5.32i ⊢ ( ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) ↔ ( Rel 𝐹 ∧ 𝐹 ⊆ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
30 dffun4 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
31 sscoid ⊢ ( 𝐹 ⊆ ( I ∘ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) ↔ ( Rel 𝐹 ∧ 𝐹 ⊆ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )
32 29 30 31 3bitr4i ⊢ ( Fun 𝐹 ↔ 𝐹 ⊆ ( I ∘ ( V ∖ ( ( V ∖ I ) ∘ 𝐹 ) ) ) )