Theorem dffun10

Description: Another potential definition of functionhood. 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 ) ∘ 𝐹 ) ) ) )