Metamath Proof Explorer

Theorem tgjustf

Description: Given any function F , equality of the image by F is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023)

Ref Expression
Assertion tgjustf ( 𝐴 ∈ 𝑉 → ∃ 𝑟 ( 𝑟 Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) }
2 ancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
3 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
4 2 3 anbi12i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
5 simpl ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → 𝑢 = 𝑥 )
6 5 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑥 ) )
7 simpr ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → 𝑣 = 𝑦 )
8 7 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
9 6 8 eqeq12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
10 eqid ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) }
11 9 10 brab2a ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
12 simpl ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑥 ) → 𝑢 = 𝑦 )
13 12 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑥 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑦 ) )
14 simpr ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑥 ) → 𝑣 = 𝑥 )
15 14 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑥 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑥 ) )
16 13 15 eqeq12d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑥 ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
17 16 10 brab2a ⊢ ( 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑥 ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
18 4 11 17 3bitr4i ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑥 )
19 18 biimpi ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 → 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑥 )
20 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑥 ∈ 𝐴 )
21 simprlr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
22 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
23 simprr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
24 22 23 eqtrd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
25 20 21 24 jca31 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) )
26 simpl ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → 𝑢 = 𝑦 )
27 26 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑦 ) )
28 simpr ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → 𝑣 = 𝑧 )
29 28 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑧 ) )
30 27 29 eqeq12d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
31 30 10 brab2a ⊢ ( 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑧 ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
32 11 31 anbi12i ⊢ ( ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ∧ 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) ) )
33 simpl ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑧 ) → 𝑢 = 𝑥 )
34 33 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑧 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑥 ) )
35 simpr ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑧 ) → 𝑣 = 𝑧 )
36 35 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑧 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑧 ) )
37 34 36 eqeq12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑧 ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) )
38 37 10 brab2a ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) )
39 25 32 38 3imtr4i ⊢ ( ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ∧ 𝑦 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑧 ) → 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑧 )
40 eqid ⊢ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
41 40 biantru ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
42 pm4.24 ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
43 simpl ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑥 ) → 𝑢 = 𝑥 )
44 43 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑥 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑥 ) )
45 simpr ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑥 ) → 𝑣 = 𝑥 )
46 45 fveq2d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑥 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑥 ) )
47 44 46 eqeq12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑥 ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
48 47 10 brab2a ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑥 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
49 41 42 48 3bitr4i ⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑥 )
50 1 19 39 49 iseri ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } Er 𝐴
51 11 baib ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
52 51 rgen2 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
53 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
54 simprll ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) ) → 𝑢 ∈ 𝐴 )
55 simprlr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) ) → 𝑣 ∈ 𝐴 )
56 53 53 54 55 opabex2 ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } ∈ V )
57 ereq1 ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } → ( 𝑟 Er 𝐴 ↔ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } Er 𝐴 ) )
58 simpl ⊢ ( ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } )
59 58 breqd ⊢ ( ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑟 𝑦 ↔ 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ) )
60 59 bibi1d ⊢ ( ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
61 60 2ralbidva ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
62 57 61 anbi12d ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } → ( ( 𝑟 Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
63 62 spcegv ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } ∈ V → ( ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑟 ( 𝑟 Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
64 56 63 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) } 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑟 ( 𝑟 Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
65 50 52 64 mp2ani ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑟 ( 𝑟 Er 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑟 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )