| Step | Hyp | Ref | Expression | 
						
							| 1 |  | constr0.1 | ⊢ 𝐶  =  rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) | 
						
							| 2 |  | constrsuc.1 | ⊢ ( 𝜑  →  𝑁  ∈  On ) | 
						
							| 3 |  | constrsuc.2 | ⊢ 𝑆  =  ( 𝐶 ‘ 𝑁 ) | 
						
							| 4 | 1 | fveq1i | ⊢ ( 𝐶 ‘ suc  𝑁 )  =  ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ suc  𝑁 ) | 
						
							| 5 |  | rdgsuc | ⊢ ( 𝑁  ∈  On  →  ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ suc  𝑁 )  =  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) ) ) | 
						
							| 6 | 2 5 | syl | ⊢ ( 𝜑  →  ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ suc  𝑁 )  =  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) ) ) | 
						
							| 7 | 4 6 | eqtrid | ⊢ ( 𝜑  →  ( 𝐶 ‘ suc  𝑁 )  =  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) ) ) | 
						
							| 8 | 1 | fveq1i | ⊢ ( 𝐶 ‘ 𝑁 )  =  ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) | 
						
							| 9 | 3 8 | eqtri | ⊢ 𝑆  =  ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) | 
						
							| 10 | 9 | fveq2i | ⊢ ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ 𝑆 )  =  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ ( rec ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ,  { 0 ,  1 } ) ‘ 𝑁 ) ) | 
						
							| 11 | 7 10 | eqtr4di | ⊢ ( 𝜑  →  ( 𝐶 ‘ suc  𝑁 )  =  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ 𝑆 ) ) | 
						
							| 12 | 11 | eleq2d | ⊢ ( 𝜑  →  ( 𝑋  ∈  ( 𝐶 ‘ suc  𝑁 )  ↔  𝑋  ∈  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ 𝑆 ) ) ) | 
						
							| 13 |  | eqid | ⊢ ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } )  =  ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) | 
						
							| 14 |  | id | ⊢ ( 𝑠  =  𝑆  →  𝑠  =  𝑆 ) | 
						
							| 15 |  | rexeq | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 16 | 14 15 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 17 | 14 16 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 18 | 14 17 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 19 |  | rexeq | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 20 | 14 19 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 21 | 14 20 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 22 | 14 21 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 23 | 14 22 | rexeqbidvv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 24 |  | rexeq | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 25 | 14 24 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 26 | 14 25 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 27 | 14 26 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 28 | 14 27 | rexeqbidv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 29 | 14 28 | rexeqbidvv | ⊢ ( 𝑠  =  𝑆  →  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 30 | 18 23 29 | 3orbi123d | ⊢ ( 𝑠  =  𝑆  →  ( ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) )  ↔  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) | 
						
							| 31 | 30 | rabbidv | ⊢ ( 𝑠  =  𝑆  →  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  =  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) | 
						
							| 32 | 31 | adantl | ⊢ ( ( 𝜑  ∧  𝑠  =  𝑆 )  →  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  =  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) | 
						
							| 33 | 3 | fvexi | ⊢ 𝑆  ∈  V | 
						
							| 34 | 33 | a1i | ⊢ ( 𝜑  →  𝑆  ∈  V ) | 
						
							| 35 |  | cnex | ⊢ ℂ  ∈  V | 
						
							| 36 |  | ssrab2 | ⊢ { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ⊆  ℂ | 
						
							| 37 | 35 36 | ssexi | ⊢ { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ∈  V | 
						
							| 38 | 37 | a1i | ⊢ ( 𝜑  →  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ∈  V ) | 
						
							| 39 | 13 32 34 38 | fvmptd2 | ⊢ ( 𝜑  →  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ 𝑆 )  =  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) | 
						
							| 40 | 39 | eleq2d | ⊢ ( 𝜑  →  ( 𝑋  ∈  ( ( 𝑠  ∈  V  ↦  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑠 ∃ 𝑏  ∈  𝑠 ∃ 𝑐  ∈  𝑠 ∃ 𝑑  ∈  𝑠 ∃ 𝑒  ∈  𝑠 ∃ 𝑓  ∈  𝑠 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ‘ 𝑆 )  ↔  𝑋  ∈  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) ) | 
						
							| 41 |  | eqeq1 | ⊢ ( 𝑥  =  𝑦  →  ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ↔  𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) ) ) ) | 
						
							| 42 |  | eqeq1 | ⊢ ( 𝑥  =  𝑦  →  ( 𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ↔  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) ) ) ) | 
						
							| 43 | 41 42 | 3anbi12d | ⊢ ( 𝑥  =  𝑦  →  ( ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 44 | 43 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 45 | 44 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 46 | 45 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 47 |  | fvoveq1 | ⊢ ( 𝑥  =  𝑦  →  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑦  −  𝑐 ) ) ) | 
						
							| 48 | 47 | eqeq1d | ⊢ ( 𝑥  =  𝑦  →  ( ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) )  ↔  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) | 
						
							| 49 | 41 48 | anbi12d | ⊢ ( 𝑥  =  𝑦  →  ( ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 50 | 49 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 51 | 50 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 52 | 51 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 53 |  | fvoveq1 | ⊢ ( 𝑥  =  𝑦  →  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑦  −  𝑎 ) ) ) | 
						
							| 54 | 53 | eqeq1d | ⊢ ( 𝑥  =  𝑦  →  ( ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ↔  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) ) ) ) | 
						
							| 55 |  | fvoveq1 | ⊢ ( 𝑥  =  𝑦  →  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑦  −  𝑑 ) ) ) | 
						
							| 56 | 55 | eqeq1d | ⊢ ( 𝑥  =  𝑦  →  ( ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) )  ↔  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) | 
						
							| 57 | 54 56 | 3anbi23d | ⊢ ( 𝑥  =  𝑦  →  ( ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 58 | 57 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 59 | 58 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 60 | 59 | 2rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 61 | 46 52 60 | 3orbi123d | ⊢ ( 𝑥  =  𝑦  →  ( ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) )  ↔  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) | 
						
							| 62 | 61 | cbvrabv | ⊢ { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  =  { 𝑦  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } | 
						
							| 63 | 62 | eleq2i | ⊢ ( 𝑋  ∈  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ↔  𝑋  ∈  { 𝑦  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) } ) | 
						
							| 64 |  | eqeq1 | ⊢ ( 𝑦  =  𝑋  →  ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ↔  𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) ) ) ) | 
						
							| 65 |  | eqeq1 | ⊢ ( 𝑦  =  𝑋  →  ( 𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ↔  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) ) ) ) | 
						
							| 66 | 64 65 | 3anbi12d | ⊢ ( 𝑦  =  𝑋  →  ( ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 67 | 66 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 68 | 67 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 69 | 68 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 ) ) ) | 
						
							| 70 |  | fvoveq1 | ⊢ ( 𝑦  =  𝑋  →  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑋  −  𝑐 ) ) ) | 
						
							| 71 | 70 | eqeq1d | ⊢ ( 𝑦  =  𝑋  →  ( ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) )  ↔  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) | 
						
							| 72 | 64 71 | anbi12d | ⊢ ( 𝑦  =  𝑋  →  ( ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 73 | 72 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 74 | 73 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 75 | 74 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 76 |  | fvoveq1 | ⊢ ( 𝑦  =  𝑋  →  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑋  −  𝑎 ) ) ) | 
						
							| 77 | 76 | eqeq1d | ⊢ ( 𝑦  =  𝑋  →  ( ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ↔  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) ) ) ) | 
						
							| 78 |  | fvoveq1 | ⊢ ( 𝑦  =  𝑋  →  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑋  −  𝑑 ) ) ) | 
						
							| 79 | 78 | eqeq1d | ⊢ ( 𝑦  =  𝑋  →  ( ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) )  ↔  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) | 
						
							| 80 | 77 79 | 3anbi23d | ⊢ ( 𝑦  =  𝑋  →  ( ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 81 | 80 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 82 | 81 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 83 | 82 | 2rexbidv | ⊢ ( 𝑦  =  𝑋  →  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ↔  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) | 
						
							| 84 | 69 75 83 | 3orbi123d | ⊢ ( 𝑦  =  𝑋  →  ( ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) )  ↔  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) | 
						
							| 85 | 84 | elrab | ⊢ ( 𝑋  ∈  { 𝑦  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑦  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑦  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑦  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑦  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑦  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ↔  ( 𝑋  ∈  ℂ  ∧  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) | 
						
							| 86 | 63 85 | bitri | ⊢ ( 𝑋  ∈  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ↔  ( 𝑋  ∈  ℂ  ∧  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) | 
						
							| 87 | 86 | a1i | ⊢ ( 𝜑  →  ( 𝑋  ∈  { 𝑥  ∈  ℂ  ∣  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑥  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑥  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑥  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑥  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑥  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) }  ↔  ( 𝑋  ∈  ℂ  ∧  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) ) | 
						
							| 88 | 12 40 87 | 3bitrd | ⊢ ( 𝜑  →  ( 𝑋  ∈  ( 𝐶 ‘ suc  𝑁 )  ↔  ( 𝑋  ∈  ℂ  ∧  ( ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑡  ∈  ℝ ∃ 𝑟  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  𝑋  =  ( 𝑐  +  ( 𝑟  ·  ( 𝑑  −  𝑐 ) ) )  ∧  ( ℑ ‘ ( ( ∗ ‘ ( 𝑏  −  𝑎 ) )  ·  ( 𝑑  −  𝑐 ) ) )  ≠  0 )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ∃ 𝑡  ∈  ℝ ( 𝑋  =  ( 𝑎  +  ( 𝑡  ·  ( 𝑏  −  𝑎 ) ) )  ∧  ( abs ‘ ( 𝑋  −  𝑐 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) )  ∨  ∃ 𝑎  ∈  𝑆 ∃ 𝑏  ∈  𝑆 ∃ 𝑐  ∈  𝑆 ∃ 𝑑  ∈  𝑆 ∃ 𝑒  ∈  𝑆 ∃ 𝑓  ∈  𝑆 ( 𝑎  ≠  𝑑  ∧  ( abs ‘ ( 𝑋  −  𝑎 ) )  =  ( abs ‘ ( 𝑏  −  𝑐 ) )  ∧  ( abs ‘ ( 𝑋  −  𝑑 ) )  =  ( abs ‘ ( 𝑒  −  𝑓 ) ) ) ) ) ) ) |