Metamath Proof Explorer

Theorem elfuns

Description: Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypothesis elfuns.1 ⊢ 𝐹 ∈ V
Assertion elfuns ( 𝐹 ∈ Funs ↔ Fun 𝐹 )

Proof

Step Hyp Ref Expression
1 elfuns.1 ⊢ 𝐹 ∈ V
2 elrel ⊢ ( ( Rel 𝐹 ∧ 𝑝 ∈ 𝐹 ) → ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
3 2 ex ⊢ ( Rel 𝐹 → ( 𝑝 ∈ 𝐹 → ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
4 elrel ⊢ ( ( Rel 𝐹 ∧ 𝑞 ∈ 𝐹 ) → ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ )
5 4 ex ⊢ ( Rel 𝐹 → ( 𝑞 ∈ 𝐹 → ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) )
6 3 5 anim12d ⊢ ( Rel 𝐹 → ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) → ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ) )
7 6 adantrd ⊢ ( Rel 𝐹 → ( ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) → ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ) )
8 7 pm4.71rd ⊢ ( Rel 𝐹 → ( ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ) )
9 19.41vvvv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
10 ee4anv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) )
11 10 anbi1i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
12 9 11 bitr2i ⊢ ( ( ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑎 ∃ 𝑧 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
13 8 12 bitrdi ⊢ ( Rel 𝐹 → ( ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ) )
14 13 2exbidv ⊢ ( Rel 𝐹 → ( ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ↔ ∃ 𝑝 ∃ 𝑞 ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ) )
15 excom13 ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑥 ∃ 𝑞 ∃ 𝑝 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
16 excom13 ⊢ ( ∃ 𝑞 ∃ 𝑝 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∃ 𝑞 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
17 exrot4 ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑎 ∃ 𝑧 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
18 excom ⊢ ( ∃ 𝑎 ∃ 𝑧 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑧 ∃ 𝑎 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
19 df-3an ⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
20 19 2exbii ⊢ ( ∃ 𝑝 ∃ 𝑞 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
21 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
22 opex ⊢ ⟨ 𝑎 , 𝑧 ⟩ ∈ V
23 eleq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
24 23 anbi1d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ) )
25 breq2 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ↔ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ) )
26 24 25 anbi12d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ) ) )
27 eleq1 ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( 𝑞 ∈ 𝐹 ↔ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) )
28 27 anbi2d ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ) )
29 breq1 ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑎 , 𝑧 ⟩ ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ) )
30 vex ⊢ 𝑥 ∈ V
31 vex ⊢ 𝑦 ∈ V
32 22 30 31 brtxp ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ⟨ 𝑎 , 𝑧 ⟩ 1st 𝑥 ∧ ⟨ 𝑎 , 𝑧 ⟩ ( ( V ∖ I ) ∘ 2nd ) 𝑦 ) )
33 vex ⊢ 𝑎 ∈ V
34 vex ⊢ 𝑧 ∈ V
35 33 34 br1steq ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ 1st 𝑥 ↔ 𝑥 = 𝑎 )
36 equcom ⊢ ( 𝑥 = 𝑎 ↔ 𝑎 = 𝑥 )
37 35 36 bitri ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ 1st 𝑥 ↔ 𝑎 = 𝑥 )
38 22 31 brco ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ ( ( V ∖ I ) ∘ 2nd ) 𝑦 ↔ ∃ 𝑥 ( ⟨ 𝑎 , 𝑧 ⟩ 2nd 𝑥 ∧ 𝑥 ( V ∖ I ) 𝑦 ) )
39 33 34 br2ndeq ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ 2nd 𝑥 ↔ 𝑥 = 𝑧 )
40 39 anbi1i ⊢ ( ( ⟨ 𝑎 , 𝑧 ⟩ 2nd 𝑥 ∧ 𝑥 ( V ∖ I ) 𝑦 ) ↔ ( 𝑥 = 𝑧 ∧ 𝑥 ( V ∖ I ) 𝑦 ) )
41 40 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝑎 , 𝑧 ⟩ 2nd 𝑥 ∧ 𝑥 ( V ∖ I ) 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 ( V ∖ I ) 𝑦 ) )
42 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ( V ∖ I ) 𝑦 ↔ 𝑧 ( V ∖ I ) 𝑦 ) )
43 brv ⊢ 𝑧 V 𝑦
44 brdif ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ( 𝑧 V 𝑦 ∧ ¬ 𝑧 I 𝑦 ) )
45 43 44 mpbiran ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ¬ 𝑧 I 𝑦 )
46 31 ideq ⊢ ( 𝑧 I 𝑦 ↔ 𝑧 = 𝑦 )
47 equcom ⊢ ( 𝑧 = 𝑦 ↔ 𝑦 = 𝑧 )
48 46 47 bitri ⊢ ( 𝑧 I 𝑦 ↔ 𝑦 = 𝑧 )
49 48 notbii ⊢ ( ¬ 𝑧 I 𝑦 ↔ ¬ 𝑦 = 𝑧 )
50 45 49 bitri ⊢ ( 𝑧 ( V ∖ I ) 𝑦 ↔ ¬ 𝑦 = 𝑧 )
51 42 50 bitrdi ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ( V ∖ I ) 𝑦 ↔ ¬ 𝑦 = 𝑧 ) )
52 51 equsexvw ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 ( V ∖ I ) 𝑦 ) ↔ ¬ 𝑦 = 𝑧 )
53 38 41 52 3bitri ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ ( ( V ∖ I ) ∘ 2nd ) 𝑦 ↔ ¬ 𝑦 = 𝑧 )
54 37 53 anbi12i ⊢ ( ( ⟨ 𝑎 , 𝑧 ⟩ 1st 𝑥 ∧ ⟨ 𝑎 , 𝑧 ⟩ ( ( V ∖ I ) ∘ 2nd ) 𝑦 ) ↔ ( 𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧 ) )
55 32 54 bitri ⊢ ( ⟨ 𝑎 , 𝑧 ⟩ ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧 ) )
56 29 55 bitrdi ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧 ) ) )
57 28 56 anbi12d ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ( 𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧 ) ) ) )
58 an12 ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ( 𝑎 = 𝑥 ∧ ¬ 𝑦 = 𝑧 ) ) ↔ ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) )
59 57 58 bitrdi ⊢ ( 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) ) )
60 21 22 26 59 ceqsex2v ⊢ ( ∃ 𝑝 ∃ 𝑞 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) )
61 20 60 bitr3i ⊢ ( ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) )
62 61 exbii ⊢ ( ∃ 𝑎 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑎 ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) )
63 opeq1 ⊢ ( 𝑎 = 𝑥 → ⟨ 𝑎 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ )
64 63 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
65 64 anbi2d ⊢ ( 𝑎 = 𝑥 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) )
66 65 anbi1d ⊢ ( 𝑎 = 𝑥 → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) )
67 66 equsexvw ⊢ ( ∃ 𝑎 ( 𝑎 = 𝑥 ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑎 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) )
68 62 67 bitri ⊢ ( ∃ 𝑎 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) )
69 68 exbii ⊢ ( ∃ 𝑧 ∃ 𝑎 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) )
70 exanali ⊢ ( ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
71 69 70 bitri ⊢ ( ∃ 𝑧 ∃ 𝑎 ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
72 17 18 71 3bitri ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
73 72 exbii ⊢ ( ∃ 𝑦 ∃ 𝑝 ∃ 𝑞 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
74 exnal ⊢ ( ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
75 16 73 74 3bitri ⊢ ( ∃ 𝑞 ∃ 𝑝 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ¬ ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
76 75 exbii ⊢ ( ∃ 𝑥 ∃ 𝑞 ∃ 𝑝 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ∃ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
77 exnal ⊢ ( ∃ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
78 15 76 77 3bitri ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑥 ∃ 𝑦 ∃ 𝑎 ∃ 𝑧 ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑞 = ⟨ 𝑎 , 𝑧 ⟩ ) ∧ ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
79 14 78 bitrdi ⊢ ( Rel 𝐹 → ( ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
80 79 con2bid ⊢ ( Rel 𝐹 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ¬ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
81 80 pm5.32i ⊢ ( ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) ↔ ( Rel 𝐹 ∧ ¬ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
82 dffun4 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
83 df-funs ⊢ Funs = ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) )
84 83 eleq2i ⊢ ( 𝐹 ∈ Funs ↔ 𝐹 ∈ ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ) )
85 eldif ⊢ ( 𝐹 ∈ ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ) ↔ ( 𝐹 ∈ 𝒫 ( V × V ) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ) )
86 1 elpw ⊢ ( 𝐹 ∈ 𝒫 ( V × V ) ↔ 𝐹 ⊆ ( V × V ) )
87 df-rel ⊢ ( Rel 𝐹 ↔ 𝐹 ⊆ ( V × V ) )
88 86 87 bitr4i ⊢ ( 𝐹 ∈ 𝒫 ( V × V ) ↔ Rel 𝐹 )
89 1 elfix ⊢ ( 𝐹 ∈ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ↔ 𝐹 ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) 𝐹 )
90 1 1 coep ⊢ ( 𝐹 ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) 𝐹 ↔ ∃ 𝑝 ∈ 𝐹 𝐹 ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) 𝑝 )
91 vex ⊢ 𝑝 ∈ V
92 1 91 coepr ⊢ ( 𝐹 ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) 𝑝 ↔ ∃ 𝑞 ∈ 𝐹 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 )
93 92 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐹 𝐹 ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) 𝑝 ↔ ∃ 𝑝 ∈ 𝐹 ∃ 𝑞 ∈ 𝐹 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 )
94 90 93 bitri ⊢ ( 𝐹 ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) 𝐹 ↔ ∃ 𝑝 ∈ 𝐹 ∃ 𝑞 ∈ 𝐹 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 )
95 r2ex ⊢ ( ∃ 𝑝 ∈ 𝐹 ∃ 𝑞 ∈ 𝐹 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ↔ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) )
96 89 94 95 3bitri ⊢ ( 𝐹 ∈ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ↔ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) )
97 96 notbii ⊢ ( ¬ 𝐹 ∈ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ↔ ¬ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) )
98 88 97 anbi12i ⊢ ( ( 𝐹 ∈ 𝒫 ( V × V ) ∧ ¬ 𝐹 ∈ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) ) ↔ ( Rel 𝐹 ∧ ¬ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
99 84 85 98 3bitri ⊢ ( 𝐹 ∈ Funs ↔ ( Rel 𝐹 ∧ ¬ ∃ 𝑝 ∃ 𝑞 ( ( 𝑝 ∈ 𝐹 ∧ 𝑞 ∈ 𝐹 ) ∧ 𝑞 ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) 𝑝 ) ) )
100 81 82 99 3bitr4ri ⊢ ( 𝐹 ∈ Funs ↔ Fun 𝐹 )