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 𝐹 )